T7_threshold_bijection
For any natural number D the set of all binary patterns on D sites stands in bijection with Fin(2^D). Workers on the T7 eight-tick octave and minimal-cover counting cite the result to confirm exact saturation without aliasing at threshold cardinality. The argument obtains the Fintype equivalence to Fin of the cardinality, invokes card_pattern D for the exact count, builds explicit casts shown to be mutual inverses by case analysis, and composes to the required bijection.
claimFor every natural number $D$, there exists a bijective map from the finite set of integers modulo $2^D$ to the set of all functions from a $D$-element index set to the booleans.
background
The Patterns module develops exact counting facts for binary configurations that support the T7 eight-tick octave (period $2^3$). Pattern D is defined as the type of all maps Fin D → Bool, i.e., every possible assignment of D binary values. The sibling lemma card_pattern D establishes that this type has Fintype.card exactly equal to $2^D$. Upstream results such as the J-automorphism composition in CostAlgebra and the tick definition in Constants supply the broader Recognition Science time quantum and algebraic structure in which these pattern counts are embedded.
proof idea
The tactic proof first retrieves the Fintype equivalence e between Pattern D and Fin of its cardinality. It then uses the equality from card_pattern D to construct explicit castTo and castFrom maps between Fin(2^D) and Fin(Fintype.card Pattern D). Left and right inverses are verified by case analysis on the Fin elements, yielding a bijection on the casts. The final step composes the inverse of e with this cast bijection.
why it matters in Recognition Science
The declaration closes the exact-cardinality step required for the T7 eight-tick octave and the no-aliasing claim at threshold $2^D$. It directly supports sibling results such as eight_tick_min and T7_nyquist_obstruction. In the Recognition Science chain it supplies the discrete saturation needed for the self-similar fixed point phi and the emergence of D=3 spatial dimensions without redundancy in the pattern space.
scope and limits
- Does not construct an explicit closed-form bijection.
- Does not treat infinite D or continuous pattern spaces.
- Does not incorporate J-cost or the Recognition Composition Law.
- Does not address dynamical evolution or stability of patterns.
formal statement (Lean)
74theorem T7_threshold_bijection (D : Nat) : ∃ f : Fin (2 ^ D) → Pattern D, Function.Bijective f := by
proof body
Tactic-mode proof.
75 classical
76 let e := (Fintype.equivFin (Pattern D))
77 have hcard : Fintype.card (Pattern D) = 2 ^ D := by exact card_pattern D
78 -- Manual cast equivalence between Fin (2^D) and Fin (Fintype.card (Pattern D))
79 let castTo : Fin (2 ^ D) → Fin (Fintype.card (Pattern D)) :=
80 fun i => ⟨i.1, by
81 -- rewrite the goal via hcard and close with i.2
82 have : i.1 < 2 ^ D := i.2
83 simp [this]⟩
84 let castFrom : Fin (Fintype.card (Pattern D)) → Fin (2 ^ D) :=
85 fun j => ⟨j.1, by simpa [hcard] using j.2⟩
86 have hLeft : Function.LeftInverse castFrom castTo := by intro i; cases i; rfl
87 have hRight : Function.RightInverse castFrom castTo := by intro j; cases j; rfl
88 have hCastBij : Function.Bijective castTo := ⟨hLeft.injective, hRight.surjective⟩
89 refine ⟨fun i => (e.symm) (castTo i), ?_⟩
90 exact (e.symm).bijective.comp hCastBij
91
92/-‑ ## T6 alias theorems -/
93 theorem T6_exist_exact_2pow (d : Nat) : ∃ w : CompleteCover d, w.period = 2 ^ d :=
94 cover_exact_pow d
95
96 theorem T6_exist_8 : ∃ w : CompleteCover 3, w.period = 8 :=
97 period_exactly_8
98
99/-‑ ## Minimal counting facts and eight‑tick lower bound -/
100
101/-- For any dimension `d`, the exact cover of period `2^d` has positive period. -/
102 theorem T6_exist_exact_pos (d : Nat) : ∃ w : CompleteCover d, 0 < w.period := by
103 obtain ⟨w, hp⟩ := cover_exact_pow d
104 have : 0 < (2 : ℕ) ^ d := by
105 exact pow_pos (by decide : 0 < (2 : ℕ)) d
106 exact ⟨w, by simp [hp]⟩
107
108/-- The 3‑bit complete cover of period 8 has positive period. -/
109 theorem period_exactly_8_pos : ∃ w : CompleteCover 3, 0 < w.period := by
110 obtain ⟨w, hp⟩ := period_exactly_8
111 have : 0 < (8 : ℕ) := by decide
112 exact ⟨w, by simp [hp]⟩
113
114end Patterns
115end IndisputableMonolith