T4_Recognition
plain-language theorem explainer
Any ledger configuration permitting recognition events must contain at least one entry distinct from 1. Researchers working on the ground-state instability and the derived T6 requirement invoke this to exclude uniform initial states from the T0-T8 chain. The declaration is introduced as a structure whose single field encodes the non-triviality condition.
Claim. Let $c$ be a configuration of $N$ positive real ledger entries. The recognition condition holds for $c$ precisely when its entries are not all equal to 1.
background
The module derives that the ground state at unity is the source of all structure rather than passive equilibrium. A Configuration is a structure holding $N$ ledger entries, each a positive real ratio, together with the total defect given by the sum of individual J-costs. The local setting states that T4 Recognition Forcing requires distinguishing states and therefore excludes the uniform ledger where every entry equals 1.
proof idea
The declaration is a structure definition whose single field requires the configuration to satisfy the non-triviality predicate. No additional lemmas or tactics are applied.
why it matters
This supplies the T4 slot in the forcing chain and is used by the ground state paradox, the static ground state impossibility theorem, stillness_is_creative, and the derived T6 requirement. It shows recognition forces departure from the initial unity configuration, consistent with the Law of Existence and the eight-tick octave. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.