Marked-Prefix Potential Certificates

Abstract

Every accepted marked-prefix path satisfies its shape or charge bound.

Definition 1.1 (The complete marked-prefix product graph).

$$\forall i\in \mathbb{N},\mathrm{prefixTable}\left(i\right):\mathrm{List}\left(\mathbb{Z}\right)\times \mathrm{List}\left(\mathbb{N}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right)\times \mathrm{Option}\left(\mathbb{Z}\right)\times \mathrm{Option}\left(\mathbb{Z}\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefixTable (✓ std3).

Source. Repository-derived.

Commentary.

For indices zero through 4261, prefixTable selects one of 4262 literal rows through a balanced tree of index comparisons. The initial subtree remains inline; the other 255 subtrees are private prefixTableChunk functions taking the original natural index. Each row lists the eight-component marker state, every labelled product edge, and the two optional potentials. The components are the base-state index, marker phase, flip flag, marker parity, retained flag, input phase, output phase and bad flag. Outside this range the final row is returned; all paths use Fin 4262.

Definition 1.2 (The literal marker-state update).

$$\forall full\in \mathrm{List}\left(\mathbb{Z}\right),\forall e\in \mathbb{N}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z},\mathrm{nextMarker}\left(full,e\right)=(\lambda old:\mathrm{List}\left(\mathbb{Z}\right)\mapsto (\lambda next:\mathrm{List}\left(\mathbb{Z}\right)\mapsto (\lambda nd:\mathbb{Z}\mapsto (\lambda jd:\mathbb{Z}\mapsto (\lambda m:\mathbb{Z}\mapsto (\lambda flip:\mathrm{Bool}\mapsto (\lambda parity:\mathbb{Z}\mapsto (\lambda keep:\mathbb{Z}\mapsto (\lambda ni:\mathbb{Z}\mapsto (\lambda nj:\mathbb{Z}\mapsto (\lambda bad:\mathrm{Bool}\mapsto (\lambda finish:\mathrm{List}\left(\mathbb{Z}\right)\to \mathrm{List}\left(\mathbb{Z}\right)\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto \mathrm{ite}\left((\mathrm{getD}\left(\mathrm{ite}\left(18<List.length\left(next\right),\mathrm{some}\left(GetElem.getElem\left(next,18\right)\right),\mathrm{none}\left(\right)\right),0\right)!=0),[],\mathrm{ite}\left(m=0,(\lambda unmarked:\mathrm{List}\left(\mathbb{Z}\right)\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto \mathrm{ite}\left(\left(nd=1\wedge \mathrm{getD}\left(\mathrm{ite}\left(10<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,10\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\right)\wedge \mathrm{getD}\left(\mathrm{ite}\left(11<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,11\right)\right),\mathrm{none}\left(\right)\right),0\right)=0,[unmarked,(\lambda an:\mathrm{Bool}\mapsto (\lambda aj:\mathrm{Bool}\mapsto (\lambda kp:\mathrm{Bool}\mapsto (\lambda bd:\mathrm{Bool}\mapsto finish\left([\mathrm{cast}\left(\mathrm{fst}\left(e\right),\mathbb{Z}\right),1,\mathrm{cast}\left(\mathrm{toNat}\left(flip\right),\mathbb{Z}\right),\mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,1\right)\right),\mathrm{none}\left(\right)\right),0\right),\mathrm{cast}\left(\mathrm{toNat}\left(kp\right),\mathbb{Z}\right),\mathrm{cast}\left(\mathrm{toNat}\left(an\right),\mathbb{Z}\right),\mathrm{cast}\left(\mathrm{toNat}\left(aj\right),\mathbb{Z}\right),\mathrm{cast}\left(\mathrm{toNat}\left(bd\right),\mathbb{Z}\right)]\right))\left(Bool.or\left(Bool.or\left(Bool.or\left((\mathrm{getD}\left(\mathrm{ite}\left(12<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,12\right)\right),\mathrm{none}\left(\right)\right),0\right)!=0),(\mathrm{getD}\left(\mathrm{ite}\left(13<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,13\right)\right),\mathrm{none}\left(\right)\right),0\right)!=0)\right),Bool.and\left((jd!=0),(jd!=1)\right)\right),Bool.and\left(Bool.not\left(kp\right),Bool.or\left(Bool.or\left(Bool.not\left(an\right),aj\right),Bool.not\left(flip\right)\right)\right)\right)\right))\left((jd==1)\right))\left(Bool.or\left(\mathrm{decide}\left(\mathrm{getD}\left(\mathrm{ite}\left(17<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,17\right)\right),\mathrm{none}\left(\right)\right),0\right)<0\right),Bool.and\left((\mathrm{getD}\left(\mathrm{ite}\left(17<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,17\right)\right),\mathrm{none}\left(\right)\right),0\right)==0),(\mathrm{getD}\left(\mathrm{ite}\left(3<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,3\right)\right),\mathrm{none}\left(\right)\right),0\right)==1)\right)\right)\right))\left(Bool.or\left(\mathrm{decide}\left(\mathrm{getD}\left(\mathrm{ite}\left(16<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,16\right)\right),\mathrm{none}\left(\right)\right),0\right)<0\right),Bool.and\left((\mathrm{getD}\left(\mathrm{ite}\left(16<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,16\right)\right),\mathrm{none}\left(\right)\right),0\right)==0),(\mathrm{getD}\left(\mathrm{ite}\left(2<List.length\left(old\right),\mathrm{some}\left(GetElem.getElem\left(old,2\right)\right),\mathrm{none}\left(\right)\right),0\right)==1)\right)\right)\right)],[unmarked]\right))\left(finish\left([\mathrm{cast}\left(\mathrm{fst}\left(e\right),\mathbb{Z}\right),0,\mathrm{cast}\left(\mathrm{toNat}\left(Bool.and\left(flip,(nd+jd==0)\right)\right),\mathbb{Z}\right),0,0,0,0,0]\right)\right),\mathrm{ite}\left(m=1\vee m=2,\mathrm{ite}\left((nd!=0),[],[finish\left([\mathrm{cast}\left(\mathrm{fst}\left(e\right),\mathbb{Z}\right),m+1,\mathrm{cast}\left(\mathrm{toNat}\left(flip\right),\mathbb{Z}\right),parity,keep,ni,nj,\mathrm{cast}\left(\mathrm{toNat}\left(Bool.or\left(bad,(nd!=jd)\right)\right),\mathbb{Z}\right)]\right)]\right),\mathrm{ite}\left(m=3,\mathrm{ite}\left(Bool.and\left((nd!=0),(nd!=1)\right),[],[finish\left([\mathrm{cast}\left(\mathrm{fst}\left(e\right),\mathbb{Z}\right),\mathrm{ite}\left(nd=1,1,4\right),\mathrm{cast}\left(\mathrm{toNat}\left(flip\right),\mathbb{Z}\right),parity,keep,ni,nj,\mathrm{cast}\left(\mathrm{toNat}\left(Bool.or\left(bad,(nd!=jd)\right)\right),\mathbb{Z}\right)]\right)]\right),\mathrm{ite}\left((nd!=0),[],[finish\left([\mathrm{cast}\left(\mathrm{fst}\left(e\right),\mathbb{Z}\right),4,\mathrm{cast}\left(\mathrm{toNat}\left(flip\right),\mathbb{Z}\right),parity,keep,ni,nj,\mathrm{cast}\left(\mathrm{toNat}\left(Bool.or\left(bad,(nd!=jd)\right)\right),\mathbb{Z}\right)]\right)]\right)\right)\right)\right)\right))\left(\lambda state:\mathrm{List}\left(\mathbb{Z}\right)\mapsto (state,\mathrm{fst}\left(\mathrm{snd}\left(e\right)\right),\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{snd}\left(e\right)\right)\right),\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{snd}\left(\mathrm{snd}\left(e\right)\right)\right)\right),\mathrm{snd}\left(\mathrm{snd}\left(\mathrm{snd}\left(\mathrm{snd}\left(e\right)\right)\right)\right))\right))\left((\mathrm{getD}\left(\mathrm{ite}\left(7<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,7\right)\right),\mathrm{none}\left(\right)\right),0\right)!=0)\right))\left(\mathrm{getD}\left(\mathrm{ite}\left(6<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,6\right)\right),\mathrm{none}\left(\right)\right),0\right)\right))\left(\mathrm{getD}\left(\mathrm{ite}\left(5<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,5\right)\right),\mathrm{none}\left(\right)\right),0\right)\right))\left(\mathrm{getD}\left(\mathrm{ite}\left(4<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,4\right)\right),\mathrm{none}\left(\right)\right),0\right)\right))\left(\mathrm{getD}\left(\mathrm{ite}\left(3<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,3\right)\right),\mathrm{none}\left(\right)\right),0\right)\right))\left((\mathrm{getD}\left(\mathrm{ite}\left(2<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,2\right)\right),\mathrm{none}\left(\right)\right),0\right)!=0)\right))\left(\mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,1\right)\right),\mathrm{none}\left(\right)\right),0\right)\right))\left(\mathrm{getD}\left(\mathrm{ite}\left(12<List.length\left(next\right),\mathrm{some}\left(GetElem.getElem\left(next,12\right)\right),\mathrm{none}\left(\right)\right),0\right)\right))\left(\mathrm{getD}\left(\mathrm{ite}\left(10<List.length\left(next\right),\mathrm{some}\left(GetElem.getElem\left(next,10\right)\right),\mathrm{none}\left(\right)\right),0\right)\right))\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{fst}\left(e\right)\right)\right)\right))\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{toNat}\left(\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,0\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.nextMarker (✓ std3).

Source. Repository-derived.

Commentary.

The marker modes are zero before selection, one and two while reading the two separating zeros, three before the next positive coefficient, and four during the final zeros. The formula displays the complete branch update. Each Boolean flag is converted to a natural number and then to an integer for storage.

Definition 1.3 (Literal marker transitions).

$$\forall full\in \mathrm{List}\left(\mathbb{Z}\right),\mathrm{successors}\left(full\right)=\mathrm{flatMap}\left(e:\mathbb{N}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto \mathrm{nextMarker}\left(full,e\right),\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{baseTable}\left(\mathrm{toNat}\left(\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,0\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.successors (✓ std3).

Source. Repository-derived.

Commentary.

Every base edge is passed to the marker-state transition nextMarker. The unmarked phase may remain unmarked or select a positive digit with two preceding zeros; marked phases read two zeros and the next positive digit, and phase four flushes leading zeros. Output-class violations are excluded and the flip, phase, parity, retention and bad flags follow the literal marker update.

Definition 1.4 (The successor-completeness checker).

$$\forall i\in \mathbb{N},\mathrm{prefixRealizationRowCheck}\left(i\right)=Bool.and\left(\mathrm{all}\left(a:\mathrm{List}\left(\mathbb{Z}\right)\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto \mathrm{contains}\left(\mathrm{map}\left(e:\mathbb{N}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto (\mathrm{fst}\left(\mathrm{prefixTable}\left(\mathrm{fst}\left(e\right)\right)\right),\mathrm{snd}\left(e\right)),\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{prefixTable}\left(i\right)\right)\right)\right),a\right),\mathrm{successors}\left(\mathrm{fst}\left(\mathrm{prefixTable}\left(i\right)\right)\right)\right),\mathrm{all}\left(e:\mathbb{N}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto \mathrm{decide}\left(\mathrm{fst}\left(e\right)<4262\right),\mathrm{fst}\left(\mathrm{snd}\left(\mathrm{prefixTable}\left(i\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefixRealizationRowCheck (✓ std3).

Source. Repository-derived.

Commentary.

The checker compares every literal marker successor against the decoded indexed edge list, then verifies every target index is below 4262. It checks transition completeness independently of the potential inequalities.

Definition 1.5 (Bounded reconstruction windows).

$$\forall start\in \mathbb{N},\forall count\in \mathbb{N},\mathrm{prefixRealizationBlockCheck}\left(start,count\right)=\mathrm{all}\left(k:\mathbb{N}\mapsto \mathrm{prefixRealizationRowCheck}\left(start+k\right),\mathrm{range}\left(count\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefixRealizationBlockCheck (✓ std3).

Source. Repository-derived.

Commentary.

Each window checks count consecutive rows starting at start. Separate kernel certificates cover all windows, and their union covers every marker state.

Definition 1.6 (Completed marker and terminal base state).

$$\forall full\in \mathrm{List}\left(\mathbb{Z}\right),\mathrm{terminal}\left(full\right)=Bool.and\left((\mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,1\right)\right),\mathrm{none}\left(\right)\right),0\right)==4),\mathrm{baseTerminal}\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{toNat}\left(\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,0\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.terminal (✓ std3).

Source. Repository-derived.

Commentary.

The terminal test requires marker phase four and a terminal underlying base state. The bad flag is tested separately by each automaton’s acceptance predicate. Option lookups use default zero and toNat converts the stored integer index to a natural number.

Definition 1.7 (The terminal marked-prefix charge correction).

$$\forall full\in \mathrm{List}\left(\mathbb{Z}\right),\mathrm{prefixOffset}\left(full\right)=\mathrm{baseOffset}\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{toNat}\left(\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,0\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\right)\right)+\mathrm{ite}\left((\mathrm{getD}\left(\mathrm{ite}\left(4<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,4\right)\right),\mathrm{none}\left(\right)\right),0\right)!=0),(1+2\cdot \mathrm{getD}\left(\mathrm{ite}\left(3<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,3\right)\right),\mathrm{none}\left(\right)\right),0\right)-1)\cdot (\mathrm{getD}\left(\mathrm{ite}\left(6<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,6\right)\right),\mathrm{none}\left(\right)\right),0\right)-\mathrm{getD}\left(\mathrm{ite}\left(5<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,5\right)\right),\mathrm{none}\left(\right)\right),0\right)),1+2\cdot \mathrm{getD}\left(\mathrm{ite}\left(3<List.length\left(full\right),\mathrm{some}\left(GetElem.getElem\left(full,3\right)\right),\mathrm{none}\left(\right)\right),0\right)+1\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefixOffset (✓ std3).

Source. Repository-derived.

Commentary.

The terminal correction adds the base charge offset to the contribution of the retained or removed lowest marked digit. The marker parity assigns weight one or three. The operator getD reads an optional list entry with default zero, toNat converts an integer index to a natural number, and bne is Boolean inequality.

Definition 1.8 (The marked-prefix automata).

$$\forall charge\in \mathrm{Bool},\mathrm{prefixAutomaton}\left(charge\right)=NFA.mk\left(i:\mathrm{Fin}\left(4262\right)\mapsto a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\mapsto \{j:\mathrm{Fin}\left(4262\right)\mid (\mathrm{val}\left(j\right),a)\in \mathrm{fst}\left(\mathrm{snd}\left(\mathrm{prefixTable}\left(\mathrm{val}\left(i\right)\right)\right)\right)\},\{i:\mathrm{Fin}\left(4262\right)\mid \mathrm{val}\left(i\right)<5\},\{i:\mathrm{Fin}\left(4262\right)\mid Bool.and\left(Bool.and\left((\mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(\mathrm{fst}\left(\mathrm{prefixTable}\left(\mathrm{val}\left(i\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{prefixTable}\left(\mathrm{val}\left(i\right)\right)\right),1\right)\right),\mathrm{none}\left(\right)\right),0\right)==4),\mathrm{baseTerminal}\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{toNat}\left(\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(\mathrm{fst}\left(\mathrm{prefixTable}\left(\mathrm{val}\left(i\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{prefixTable}\left(\mathrm{val}\left(i\right)\right)\right),0\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\right)\right)\right),(\mathrm{getD}\left(\mathrm{ite}\left(7<List.length\left(\mathrm{fst}\left(\mathrm{prefixTable}\left(\mathrm{val}\left(i\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{prefixTable}\left(\mathrm{val}\left(i\right)\right)\right),7\right)\right),\mathrm{none}\left(\right)\right),0\right)==\mathrm{ite}\left(charge,0,1\right))\right)\}\right)$$

Formalization. D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefixAutomaton (✓ std3).

Source. Repository-derived.

Commentary.

Both modes start at indices zero through four and use every listed product edge. Acceptance requires the marker phase to be four, a terminal base state, and bad flag zero for the charge mode or one for the shape mode. The Boolean parameter chooses the mode.

Theorem 1.9 (Bounds on every accepted marked-prefix path).

$$\forall charge\in \mathrm{Bool},\forall s\in \mathrm{Fin}\left(4262\right),\forall t\in \mathrm{Fin}\left(4262\right),\forall xs\in \mathrm{List}\left(\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right),\left(s\in \mathrm{start}\left(\mathrm{prefixAutomaton}\left(charge\right)\right)\wedge t\in \mathrm{accept}\left(\mathrm{prefixAutomaton}\left(charge\right)\right)\right)\Rightarrow \left(\forall p\in \mathrm{Path}\left(\mathrm{prefixAutomaton}\left(charge\right),s,t,xs\right),\mathrm{pathCharge}\left(\lambda [\mathrm{Fin}\left(4262\right)]a:\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}[\mathrm{Fin}\left(4262\right)]\mapsto \mathrm{ite}\left(charge,5,1\right)\cdot \mathrm{fst}\left(a\right)+\mathrm{ite}\left(charge,\mathrm{fst}\left(\mathrm{snd}\left(a\right)\right),0\right),p\right)+\mathrm{ite}\left(charge,\mathrm{prefixOffset}\left(\mathrm{fst}\left(\mathrm{prefixTable}\left(\mathrm{val}\left(t\right)\right)\right)\right),0\right)\le \mathrm{ite}\left(charge,5,0\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefix_accepted_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The shape mode bounds total f charge by zero. The charge mode bounds five times f charge plus q charge and the terminal marked-prefix correction by five. The potentials telescope along paths of arbitrary length. Identifying these graph labels with integer cuts and signed-digit charges is a separate arithmetic obligation.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.nextMarker
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefixAutomaton
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefixOffset
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefixRealizationBlockCheck
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefixRealizationRowCheck
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefixTable
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.prefix_accepted_bound
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.successors
• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixCertificates.terminal
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseCertificates