posting_coefficients_minimal
plain-language theorem explainer
The unit pair of posting coefficients satisfies max(1,1)=1 as its minimal value. Researchers deriving integer coefficients for scale hierarchies under the Recognition Composition Law cite this base case to anchor discrete Fibonacci sequences. The proof reduces the equality by direct simplification.
Claim. $max(1,1)=1$
background
The PostingExtensivity module starts from the Recognition Composition Law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y) with J(x)=(x+x^{-1})/2-1. It introduces the posting potential Π(x):=J(x)+1=½(x+x^{-1}), which satisfies the multiplicative d'Alembert relation Π(ab)+Π(a/b)=2Π(a)Π(b). This forces additive scale composition ℓ_{k+2}=ℓ_{k+1}+ℓ_k once the sequence is closed under the first composition step, closing Proposition 4.3 without assuming linearity a priori.
proof idea
The proof is a one-line wrapper that applies the simplifier to the equality max(1,1)=1.
why it matters
This base case anchors the integer-coefficients step (discrete_coefficients) that feeds discrete_fibonacci_from_minimality and posting_gives_unit_recurrence. It supplies the minimal natural-number coefficients required for the additive recurrence derived from the RCL in the phi-ladder construction, directly supporting the self-similar fixed point and eight-tick octave of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.