T7_threshold_bijection
Recognition Science requires a bijection between Fin (2^D) and the space of all binary assignments on D positions at the T7 threshold. Researchers modeling the eight-tick octave cite the result to guarantee that every pattern is reached exactly once with no aliasing. The tactic proof obtains the cardinality equality from card_pattern, builds explicit casts between the two Fin types, and composes them with Fintype.equivFin.
claimFor any natural number $D$, there exists a bijection $f : Fin(2^D) → (Fin D → Bool)$.
background
Pattern D is defined as the type of all functions from Fin D to Bool, i.e., the set of all binary strings of length D. In the Patterns module these objects label discrete states traversed during each period of the eight-tick octave. The declaration comment states that at threshold T = 2^D the pattern space admits a bijection with no aliasing, placing the result inside the T7 block of the forcing chain.
proof idea
The proof runs in tactic mode. It invokes classical, obtains the standard equivalence e := Fintype.equivFin (Pattern D), and pulls the cardinality fact hcard : Fintype.card (Pattern D) = 2^D from card_pattern. It defines castTo and castFrom that transport between Fin (2^D) and Fin (Fintype.card (Pattern D)) while preserving bounds, proves they are mutual inverses by case analysis on the Fin elements, and refines the target bijection as the composition of e.symm with the cast bijection.
why it matters in Recognition Science
The declaration supplies the T7 threshold bijection step, confirming that the pattern count reaches exactly 2^D without aliasing. It supports the eight-tick octave (period 2^3) and the emergence of D = 3 spatial dimensions in the UnifiedForcingChain. With zero downstream uses it functions as a foundational counting fact rather than feeding a specific later theorem.
scope and limits
- Does not assert that any particular bijection is canonical or structure-preserving.
- Does not extend the statement beyond finite natural numbers D.
- Does not connect the bijection to J-automorphisms or cost composition.
- Does not address infinite-dimensional pattern spaces.
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