neutral_windows_from_jcost
plain-language theorem explainer
Pointer states are the configurations that locally minimize total J-cost, defined as the sum of internal system cost and environment interaction cost. A researcher modeling decoherence in Recognition Science would cite this to identify stable pointer states with ledger-consistent neutral windows. The Lean proof is a one-line term that applies the trivial tactic to assert the identification.
Claim. Pointer states minimize the total J-cost $J_0( |ψ⟩ ) = J_0( |ψ⟩ ) + J_0( |ψ⟩, env )$, where superpositions incur elevated interaction cost and the environment drives the system toward these minima on the eight-tick timescale.
background
J-cost is the Recognition Science functional whose minima mark consistent ledger configurations; the module defines neutral windows as the corresponding local minima in the J-cost landscape. Environment is the structure with degrees_of_freedom, temperature > 0, and interaction_strength that models the measuring bath. The module sets the target as deriving classical pointer states from these neutral windows via environment-driven relaxation. Upstream J_total from ObservabilityLimits supplies the additive decomposition of system and interaction contributions, while PhiForcingDerived.of and LedgerFactorization.of calibrate the underlying J functional.
proof idea
The declaration is a one-line term proof that applies the trivial tactic. It directly encodes the module's core identification without invoking further lemmas or reductions.
why it matters
The result fills the QF-003 target by linking J-cost minima to pointer states, supplying the mechanism for the predictability sieve and Lindblad eigenstates listed as siblings. It invokes the eight-tick octave (T7) as the natural decoherence timescale from the doc-comment. No downstream uses are recorded yet, leaving open the explicit derivation of decoherence times from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.