T4_AnalyticRecognition_Refinement
plain-language theorem explainer
Analytic refinement of the T4 recognition step: a five-field Prop packaging necessity of recognition for nonconstant observables, extraction mechanisms as recognition structures, events as scalar cost configurations, cost minima as events, and J-stability forcing recognition structure. Downstream chain theorems cite it to discharge T4 and bridge into T5 uniqueness of J. Definitional interface only; the inhabiting theorem lives separately.
Claim. A proposition with five conjuncts. (1) For any state space $S$ and observable on $S$, if the observable is nonconstant then there exist types $R_1,R_2$ admitting a recognition between them. (2) Every observable-extraction mechanism on $S$ yields a recognition structure on $S$. (3) For a ledger recognition event $e$: $e$ has ratio $1$ iff its recognition cost is $0$, and ratio $\neq 1$ implies strictly positive cost. (4) Every configuration value is realized as the ratio of some recognition event. (5) Every $J$-stable structure has a recognition-like structure on the same carrier.
background
The Unified Forcing Chain module argues that T-1 through T8 are forced from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). In that ladder, T4 is the recognition step: once a ledger exists, observables and cost force recognition as a structure, not an extra postulate.
A recognition event is a directed pair of agents with a positive real ratio. Configurations are finite tuples of positive ledger ratios; total defect is the sum of individual $J$-costs. Recognition cost on an event is the scalar cost of its ratio (the doubled $J$-cost under a ratio weight in the engine). The analytic refinement assumes scalar $J$ recognition events already exist and restates the older observable / $J$-stability recognition package in that language.
Upstream pieces supply the vocabulary: ledger recognition events, configuration carriers, multiplicative-recognizer and rung-coarsen cost maps, and magnitude-of-mismatch forcing for single-valued comparison.
proof idea
No proof body: this is a Prop-valued structure (definitional interface). The five fields are named hypotheses, not derived here. Inhabitation is deferred to the sibling theorem that applies RecognitionForcing.recognition_forcing_complete and projects its five components into necessity, uniqueness, cost_structure, cost_minima, and stability.
why it matters
T4 sits in the complete inevitability chain between ledger forcing (T3) and unique $J$ (T5). This refinement is the analytic face of T4 once scalar $J$ events are on the table: recognition is necessary for nonconstant observables, extraction is recognition-shaped, events match cost zeros and positives, minima are events, and $J$-stability yields recognition-like structure.
It is consumed by the theorem that the refinement holds, and by the T5-to-analytic-refinements bridge certificate. That bridge records that all five analytic-refinement structures rest on the closed-form reciprocal cost $(x+x^{-1})/2-1$, whose uniqueness is T5. Without this interface, the chain cannot hand T4 off cleanly to J-uniqueness, $\varphi$ forcing, the eight-tick octave, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.