theorem
proved
term proof
metaForcedArithmeticInvariance_self
show as:
view Lean formalization →
formal statement (Lean)
119theorem metaForcedArithmeticInvariance_self (R : MetaCarrier) :
120 metaForcedArithmeticInvariance R R = Equiv.refl R.Orbit := by
proof body
Term-mode proof.
121 -- Both sides are the canonical NNO equivalence from R to itself,
122 -- which by uniqueness is the identity.
123 apply Equiv.ext
124 intro n
125 -- The NNO equivalence applied at n satisfies the universal property
126 -- of the recursor: it is the unique map R.Orbit → R.Orbit sending
127 -- orbitZero to orbitZero and intertwining orbitStep. The identity
128 -- is one such map. By uniqueness, the canonical equivalence equals
129 -- the identity.
130 unfold metaForcedArithmeticInvariance universal_forcing_via_NNO
131 IsNaturalNumberObject.equiv
132 simp only [Equiv.refl_apply, Equiv.coe_fn_mk]
133 -- Use the recursor uniqueness: the recursor with target (R.orbitZero, R.orbitStep)
134 -- is the identity.
135 have h_id_zero : (id : R.Orbit → R.Orbit) R.orbitZero = R.orbitZero := rfl
136 have h_id_step : ∀ k, (id : R.Orbit → R.Orbit) (R.orbitStep k) =
137 R.orbitStep ((id : R.Orbit → R.Orbit) k) := fun _ => rfl
138 have huniq := (realizationOrbit_isNNO R).recursor_unique
139 R.orbitZero R.orbitStep
140 (id : R.Orbit → R.Orbit) h_id_zero h_id_step n
141 -- huniq : id n = (realizationOrbit_isNNO R).recursor R.orbitZero R.orbitStep n
142 -- Goal : (realizationOrbit_isNNO R).recursor R.orbitZero R.orbitStep n = n
143 -- `id n` reduces to `n`.
144 simpa using huniq.symm
145
146/-! ## Meta-Realization Certificate
147
148The structural properties that a "meta-realization" of the Law-of-Logic
149framework would carry, all proved.
150-/
151
152/-- **Meta-Realization Certificate.**
153
154The Universal Forcing Meta-Theorem fits the Law-of-Logic structural shape:
155the meta-cost is identity, non-contradiction, total; and the meta-theorem
156itself supplies the forced-arithmetic-invariance condition that completes
157the structure.
158
159This is the reflexive-closure content of the framework. We do not claim
160to instantiate the heavy `LogicRealization` structure with all its
161orbit/step coherence axioms; instead, we record that every structural
162property the heavy structure would require has been independently
163proved. -/