has_definite_pointer
plain-language theorem explainer
A configuration c has a definite pointer when its recognition cost J applied to its value meets or exceeds the fixed threshold of 1. Modal physicists cite this predicate when formalizing automatic branch selection in the absence of any measurement axiom. The definition is a direct inequality that references the collapse_threshold constant and the J-cost evaluation on the configuration value.
Claim. A configuration $c$ has a definite pointer if $J(c.value) ≥ 1$, where $J$ is the recognition cost function and the threshold is the constant unity.
background
Configurations are points in a simplified recognition state space carrying a positive real value that generalizes a bond multiplier. The J-cost function, taken from the multiplicative recognizer and observer forcing layers, measures the recognition expense attached to a state. The collapse_threshold is the constant 1 that marks the onset of definiteness.
proof idea
This is a direct definition that equates the predicate to the inequality J c.value ≥ collapse_threshold. No lemmas or tactics are invoked; the body simply references the upstream collapse_threshold constant and the J-cost on the configuration value.
why it matters
The predicate is invoked by collapse_automatic to show that collapse occurs automatically once recognition cost exceeds unity, without any added measurement postulate. It supplies the modal condition for J-minimization to select a definite branch, consistent with the J-uniqueness step in the forcing chain. The definition embeds the threshold directly into the dynamics rather than treating it as an external axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.