Prefix-hit, mark-selection, anchor-selection, and interval-containment subcircuits

This module builds the four query subcircuits needed to evaluate forest_navigation_spec after the shared dictionary lookups have returned candidate mark and compressed-edge records:

• synthesis_prefix_hit: tests whether a target state appears along an available Q-step orbit prefix;
• synthesis_selected_mark: selects a hit mark's interval label word from Q candidate records;
• synthesis_selected_anchor: filters compressed-edge records by transientDepth f y ≤ transientDepth f a, combines with direct target-mark hits, and selects an anchor (a, low a, high a);
• synthesis_interval_containment: tests low a ≤ low h ∧ low h ≤ high a on unpacked (n + 1)-bit words.

Main results

• Cslib.Circuits.Boolean.Iteration.synthesis_prefix_hit
• Cslib.Circuits.Boolean.Iteration.synthesis_selected_mark
• Cslib.Circuits.Boolean.Iteration.synthesis_selected_anchor
• Cslib.Circuits.Boolean.Iteration.synthesis_interval_containment

References

• Adapted from lean/Proofs/ForestRecordQueries.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_prefix_hit {n a Q : ℕ} (s : Set (BooleanFunction a)) (trace : BitString a → Fin Q → BitString n) (target : BitString a → BitString n) (htrace : ∀ (j : Fin Q), (wires fun (z : BitString a) => trace z j) ⊆ s) (htarget : wires target ⊆ s) : Synthesis interpretation s {fun (z : BitString a) => decide (∃ (j : Fin Q), trace z j = target z)} (Q * (6 * n + 2) + 1)

Test whether a target state appears anywhere along an available orbit prefix.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_selected_mark {n a Q : ℕ} (f : BitString n → BitString n) (L : ℕ) (tables : ForestCircuitTables f L) (s : Set (BooleanFunction a)) (hz : (fun (x : BitString a) => false) ∈ s) (trace : BitString a → Fin Q → BitString n) (flags : BitString a → Fin Q → Bool) (records : BitString a → Fin Q → BitString (n + 1 + (n + 1))) (hflags : ∀ (j : Fin Q), (fun (z : BitString a) => flags z j) ∈ s) (hrec : ∀ (j : Fin Q), (wires fun (z : BitString a) => records z j) ⊆ s) (hdict : ∀ (z : BitString a) (j : Fin Q), (flags z j = true ↔ ∃ (i : Fin tables.markCount), tables.marks i = trace z j) ∧ ∀ (i : Fin tables.markCount), tables.marks i = trace z j → records z j = forestLabelWord tables.low tables.high (tables.marks i)) : ∃ (found : BooleanFunction a) (chosen : BitString a → BitString (n + 1 + (n + 1))), (∀ (z : BitString a), (found z = true → ∃ (j : Fin Q), trace z j ∈ FunctionalGraph.forestMarks f tables.H ∧ chosen z = forestLabelWord tables.low tables.high (trace z j)) ∧ ((∃ (j : Fin Q), trace z j ∈ FunctionalGraph.forestMarks f tables.H) → found z = true)) ∧ Synthesis interpretation s ({found} ∪ wires chosen) (Q * (8 * n + 9) + 1)

Select one marked vertex from a prefix and report whether any mark was seen.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_selected_anchor {n Q : ℕ} (f : BitString n → BitString n) (L : ℕ) (tables : ForestCircuitTables f L) (hQ : ∀ (j : Fin Q), ↑j ≤ 2 * L) (hQcomplete : ∀ k ≤ 2 * L, ∃ (j : Fin Q), ↑j = k) (s : Set (BooleanFunction (n + n))) (hy : wires inputRight ⊆ s) (hdy : ∀ (bit : Fin (n + 3)), (fun (z : BitString (n + n)) => (depthWord f (inputRight z)).getLsbD ↑bit) ∈ s) (yMarkFlag : BooleanFunction (n + n)) (yMarkRecord : BitString (n + n) → BitString (n + 1 + (n + 1))) (hyFlag : yMarkFlag ∈ s) (hyRec : wires yMarkRecord ⊆ s) (hyDict : ∀ (z : BitString (n + n)), (yMarkFlag z = true ↔ ∃ (i : Fin tables.markCount), tables.marks i = inputRight z) ∧ ∀ (i : Fin tables.markCount), tables.marks i = inputRight z → yMarkRecord z = forestLabelWord tables.low tables.high (tables.marks i)) (edgeFlags : BitString (n + n) → Fin Q → Bool) (edgeRecords : BitString (n + n) → Fin Q → BitString (n + (n + 1 + (n + 1)) + (n + 3))) (heFlags : ∀ (j : Fin Q), (fun (z : BitString (n + n)) => edgeFlags z j) ∈ s) (heRec : ∀ (j : Fin Q), (wires fun (z : BitString (n + n)) => edgeRecords z j) ⊆ s) (heDict : ∀ (z : BitString (n + n)) (j : Fin Q), (edgeFlags z j = true ↔ ∃ (i : Fin tables.edgeTable.count), tables.edgeTable.key i = f^[↑j] (inputRight z)) ∧ ∀ (i : Fin tables.edgeTable.count), tables.edgeTable.key i = f^[↑j] (inputRight z) → edgeRecords z j = forestAnchorWord f tables.low tables.high (tables.edgeTable.start i)) : ∃ (foundA : BooleanFunction (n + n)) (anchorState : BitString (n + n) → BitString n) (anchorLabels : BitString (n + n) → BitString (n + 1 + (n + 1))), (∀ (z : BitString (n + n)), (foundA z = true → FunctionalGraph.ForestAnchor f tables.H L (inputRight z) (anchorState z) ∧ anchorLabels z = forestLabelWord tables.low tables.high (anchorState z)) ∧ ((∃ (b : BitString n), FunctionalGraph.ForestAnchor f tables.H L (inputRight z) b) → foundA z = true)) ∧ Synthesis interpretation s ({foundA} ∪ wires anchorState ∪ wires anchorLabels) (Q * (21 * n + 28) + 2)

Filter edge-key hits by depth, add direct target-mark hits, and select one anchor record.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_interval_containment {n a : ℕ} (s : Set (BooleanFunction a)) (markLabels anchorLabels : BitString a → BitString (n + 1 + (n + 1))) (hmark : wires markLabels ⊆ s) (hanchor : wires anchorLabels ⊆ s) : Synthesis interpretation s {fun (z : BitString a) => !(forestLowWord (markLabels z)).ult (forestLowWord (anchorLabels z)) && !(forestHighWord (anchorLabels z)).ult (forestLowWord (markLabels z))} (24 * n + 27)

Compare the two unpacked interval words of the selected mark and anchor records.