t3_analytic_refinement_holds
plain-language theorem explainer
The analytic T3 ledger refinement packages four reciprocal-J facts: pointwise J-symmetry, equal event cost under reciprocity, paired log cancellation, and existence of a balanced (empty) ledger. Citers of the Unified Forcing Chain's analytic T3 layer use this bundle. The proof is pure structure assembly from existing LedgerForcing lemmas; no new algebra is performed.
Claim. The analytic refinement of T3 holds: the cost satisfies $J(x)=J(x^{-1})$ for every nonzero real $x$; every recognition event has the same cost as its reciprocal; the log-ratios of an event and its reciprocal sum to zero; and at least one balanced analytic ledger exists.
background
In the Unified Forcing Chain, T3 is the ledger step forced by cost symmetry $J(x)=J(1/x)$. Once the reciprocal scalar $J$ surface exists, an analytic refinement records the concrete ledger identities that the old reciprocal-J theorem still supplies downstream.
Here $J$ is the Recognition Science cost (classically $J(x)=(x+x^{-1})/2-1$). LedgerForcing models recognition events with positive ratios, a reciprocal operation, and event cost built from $J$. A ledger is balanced when double-entry holds; the empty ledger is the trivial balanced instance.
Upstream, LedgerForcing proves $J(x)=J(x^{-1})$ for $x\neq 0$ by direct expansion, cancels $\log r+\log(1/r)$ for reciprocal pairs, equates reciprocal event costs, and witnesses balance of the empty ledger.
proof idea
Term-mode structure construction. Each field is filled by a named LedgerForcing result: J_symmetric for the pointwise identity, reciprocity for event costs, paired_log_sum_zero for the log sum, and the pair (empty_ledger, empty_ledger_balanced) for existence of a balanced ledger. No intermediate tactics or fresh calculations.
why it matters
T3 in the forcing chain is "Ledger ← Cost symmetry." This declaration keeps the classical reciprocal-J ledger theorem available after the analytic $J$ surface appears, so later steps can cite balance and reciprocity without reopening T3.
It is consumed by t5_to_analytic_refinements_bridge_holds, whose doc states that the analytic-refinement bridge follows from T5 plus closed-form identities of the analytic $J$-scaffolding. In the primer landmarks, T5 is J-uniqueness ($J(x)=\cosh(\log x)-1$); closed analytic T3 ledger facts are part of that bridge's substrate. The module's claim is that every T0–T8 step is forced from the Recognition Composition Law with normalization and calibration; this closes the analytic side of T3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.