T3_AnalyticLedger_Refinement
plain-language theorem explainer
Analytic refinement of the T3 ledger step: four properties that package cost symmetry after the reciprocal scalar J is available. Anyone citing the complete inevitability chain (T-1 through T8) or the T5-to-refinements bridge will hit this interface. It is a Prop-valued structure, not a proved theorem; the witness theorem fills the four fields from LedgerForcing.
Claim. The analytic ledger refinement is the conjunction of: (i) $J(x)=J(x^{-1})$ for all real $x\neq 0$; (ii) every recognition event has the same cost as its reciprocal event; (iii) $\log r + \log(r^{-1})=0$ for the ratio $r$ of any event; (iv) there exists a balanced double-entry ledger (event list closed under the double-entry constraint).
background
In the Unified Forcing Chain, every step T-1 through T8 is claimed as a forced inevitability from the Recognition Composition Law plus normalization and calibration. T3 is the ledger step: cost symmetry $J(x)=J(1/x)$ forces a double-entry recognition ledger.
A recognition event carries a positive ratio; its reciprocal swaps source and target and inverts the ratio. Event cost is $J$ of that ratio. A ledger is a list of such events with a double-entry (balance) constraint; a ledger is balanced when its event list is balanced. Reciprocity is the theorem that event cost equals cost of the reciprocal, which is exactly $J$-symmetry applied to the ratio.
This structure is the analytic refinement of T3 once the reciprocal scalar $J$ surface exists. It sits downstream of LedgerForcing and CostAlgebra's reciprocal automorphism, and records the four ledger-facing consequences the rest of the chain expects.
proof idea
No proof body: this is a Prop-valued structure (four fields). The companion witness t3_analytic_refinement_holds fills them by direct appeal to LedgerForcing: $J$-symmetry, the reciprocity theorem, paired log-sum zero, and the empty ledger as a balanced witness. Treat the structure as the interface; the witness is the one-line assembly.
why it matters
T3 in the module map is "Ledger ← Cost symmetry $(J(x)=J(1/x))$". This refinement is the analytic packaging of that step after reciprocal $J$ is on the table, so later chain steps can cite a single Prop rather than four scattered lemmas.
It is consumed by the witness that the refinement holds, and by the T5-to-analytic-refinements bridge. That bridge records that all five analytic-refinement structures rest on the closed-form reciprocal cost $(x+x^{-1})/2-1$, with T5 (J-uniqueness) supplying the uniqueness theorem that forces the closed form. Without this interface, the bridge cannot name the ledger-side obligations T5 discharges.
Landmark link: T5 J-uniqueness and the Recognition Composition Law sit upstream of the closed form; T3 is the ledger consequence of symmetry alone, before uniqueness pins the exact $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.