collapse_automatic
plain-language theorem explainer
When the recognition cost of a configuration exceeds the collapse threshold, the actualization operator automatically produces either a definite pointer or a reduced cost below threshold. This removes any external measurement postulate from the modal dynamics. The term proof selects the second disjunct and reduces it by direct simplification with the normalization J(1) = 0 together with the definitions of actualization and the threshold.
Claim. If the recognition cost satisfies $J(c) ≥ τ$ for configuration $c$, where $τ$ denotes the collapse threshold, then the actualized configuration $A(c)$ either carries a definite pointer or obeys $J(A(c)) < τ$.
background
The J-cost is the recognition cost function normalized so that J(1) = 0, with reciprocal symmetry under inversion. Config is the structure carrying the parameters upsilonStar, eps_r, eps_v, eps_t, eps_a that label a physical state. Actualize maps a configuration to the J-minimizing element of its possibility set P(c), the dual of the possibility operator. The collapse threshold is the fixed cost level at which automatic selection occurs. The local setting is the modal layer of Recognition Science, where possibility and actualization together close the dynamics without an added measurement axiom.
proof idea
The term proof applies the right constructor to select the second disjunct. It then invokes simp with the definitions of Actualize, identity_config, J_at_one, and collapse_threshold, followed by norm_num to discharge the resulting numerical inequality.
why it matters
The result supplies the automatic-collapse step inside the Actualization module and is referenced by the module status report. It realizes the claim that cost-driven J-minimization replaces any measurement postulate, consistent with the J-uniqueness fixed point and the forcing chain from T5 onward. No open scaffolding remains for this specific statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.