identity_config
plain-language theorem explainer
identity_config supplies the minimal-cost configuration with value exactly 1 at any natural-number time t. Modal actualization proofs cite it to anchor the cost-minimizing successor. The definition is a direct structure constructor that discharges the log-bound constraint by simplification.
Claim. For each natural number $t$, the identity configuration is the element of Config with value $1$, positivity witness, time coordinate $t$, and log-bound satisfied since $|$log $1| = 0$.
background
Config is the structure used for modal logic development: a point with positive real value, time in ticks, and the bound $|$log(value)$| ≤ 16. In Modal.Possibility this simplified representation stands in for full LedgerState while preserving the J-cost geometry. Upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J function whose minimum at value 1 is realized here.
proof idea
One-line wrapper that constructs the Config tuple with value 1, the positivity witness one_pos, the supplied time t, and discharges the log-bound by simp on Real.log_one.
why it matters
This definition is the fixed point used by every_config_actualizes, collapse_automatic, and the adjointness theorems possibility_actualization_adjoint_minimal and possibility_actualization_adjoint_monotonic in Actualization. It supplies the zero-cost element required by the Recognition Composition Law and T5 J-uniqueness inside the eight-tick octave. Downstream geometry results such as curvature_at_identity and identity_in_ball also depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.