def
definition
PreservesJSymmetry
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.RecognitionForcing on GitHub at line 185.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
182structure RecognitionTracker where
183 events : List LedgerForcing.RecognitionEvent
184
185def PreservesJSymmetry (T : RecognitionTracker) : Prop :=
186 LedgerForcing.balanced_list T.events
187
188theorem ledger_is_minimal_recognition_tracker (T : RecognitionTracker) (hSymm : PreservesJSymmetry T) :
189 ∃ (L : LedgerForcing.Ledger), L.events = T.events :=
190 ⟨{ events := T.events, double_entry := hSymm }, rfl⟩
191
192/-! ## Part 6: Complete Bridge -/
193
194theorem cost_to_recognition_bridge :
195 (∀ x : ℝ, x ≠ 0 → LedgerForcing.J x = LedgerForcing.J x⁻¹) ∧
196 (∃ e : LedgerForcing.RecognitionEvent, e.ratio = 1 ∧ recognition_cost e = 0) ∧
197 (∀ (S : Type) (M : ObservableExtractionMechanism S), ∃ R : RecognitionStructure S, True) ∧
198 (∀ (S : JStableStructure), ∃ (R : RecognitionLikeStructure), R.carrier = S.carrier) :=
199 ⟨fun x hx => LedgerForcing.J_symmetric hx,
200 global_minimum_is_self_recognition,
201 fun _ M => ⟨recognition_from_extraction M, trivial⟩,
202 stability_forces_recognition⟩
203
204end RecognitionForcing
205end Foundation
206end IndisputableMonolith