recognition_distinguishability_status
plain-language theorem explainer
The definition registers the distinguishability requirement as a physical postulate derived from the Meta-Principle. Researchers tracing how logical MP enforces physical recognition events cite this label when classifying axioms in the registry. It is realized by a direct string assignment with no reduction or lemmas.
Claim. Recognition requires that states be distinguishable; if two states cannot be told apart then neither can recognize the other. This necessity is classified as a physical postulate derived from the Meta-Principle.
background
The Axioms module maintains an epistemic registry that separates physical postulates from mathematical facts and open problems. The Meta-Principle supplies the logical starting point; the distinguishability claim follows because recognition operates only on distinct states. Upstream, the Physical structure encodes positivity of c, ħ and G, while IntegrationGap.A fixes the active edge count per tick at 1. Cost functions from MultiplicativeRecognizerL4 and ObserverForcing assign non-negative J-cost to each recognition event on positive ratios.
proof idea
One-line definition that directly assigns the string constant to the status identifier. No lemmas or tactics are invoked.
why it matters
The declaration supplies the epistemic tag for the distinguishability postulate listed in the module table as a foundational physical postulate. It appears in LedgerNecessity.lean and supports the symmetry requirements recorded in ConstraintForcing.lean. Within the framework it aligns with the T0 forcing chain by ensuring recognition events are defined only on distinguishable states before J-cost and phi-ladder constructions begin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.