combiner_unit_diagonal
plain-language theorem explainer
The combiner P is normalized at the unit diagonal to equal 6 under zero-boundary, symmetry, and right-affine hypotheses. Ledger factorization derivations cite this calibration to anchor the scale before extracting the Recognition Composition Law. The proof is a direct term return of the supplied diagonal hypothesis.
Claim. Let $P : (0,1)^* $ be a combiner obeying $P(u,0)=2u$ for all $u$, symmetry $P(u,v)=P(v,u)$, and right-affineness (for each fixed $u$ the slice $v |-> P(u,v)$ is affine). Given the calibration $P(1,1)=6$, the equality $P(1,1)=6$ holds.
background
The Ledger Factorization module shows that contextual substitutivity together with regrouping invariance force the combiner to obey the FactorizationAssociativityGate, after which the gate yields the Recognition Composition Law polynomial. The combiner P records the total comparison cost of two recognition events. Upstream, cost is the J-cost of a RecognitionEvent (ObserverForcing.cost) or the derivedCost of a multiplicative recognizer comparator (MultiplicativeRecognizerL4.cost). The identity event sits at state 1 with zero J-cost (ObserverForcing.identity). The PrimitiveDistinction theorem reduces seven axioms to four structural conditions plus three definitional facts that underwrite these ledger properties.
proof idea
The proof is a one-line term that directly returns the hypothesis asserting the diagonal value equals 6.
why it matters
This declaration records the diagonal normalization P(1,1)=6 required for the combiner inside the ledger-to-RCL route. It closes the calibration step described in the module documentation, where the intermediate-value theorem on the strictly convex cost locates the point with J-cost 1 and the second-derivative condition on J composed with exp fixes the sum at 6. The result supports the forcing chain from substitutivity and regrouping invariance to the full Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.