pith. sign in
def

alphaProvenanceCert

definition
show as:
module
IndisputableMonolith.Foundation.AlphaDerivationExplicit
domain
Foundation
line
55 · github
papers citing
57 papers (below)

plain-language theorem explainer

alphaProvenanceCert supplies a concrete instance of the AlphaProvenanceCert structure that records the CODATA inverse fine-structure constant inside the Recognition Science band together with the forced properties of phi. A physicist checking the numerical output of the J-uniqueness chain would cite this certificate to close the alpha verification step. The definition populates the four fields by direct assignment of the codata band theorem and linarith on the phi > 1.5 lemma.

Claim. The certificate asserts that the CODATA value of the inverse fine-structure constant satisfies $137.030 < 137.036 < 137.039$, that the golden ratio satisfies $phi = (1 + sqrt(5))/2$, that $phi > 1$, and that the threshold $phi - 3/2 > 0$.

background

Recognition Science obtains the fine-structure constant from the J-uniqueness theorem, which forces phi as the unique self-similar fixed point, then extracts D = 3 from the eight-tick octave period 2^D = 8. This yields a 44-slot frequency structure whose exponential form places alpha inverse inside the interval (137.030, 137.039) that contains the CODATA value 137.036. The AlphaProvenanceCert structure packages exactly these four assertions: the band membership, the explicit value of phi, the lower bound phi > 1, and the positivity of the threshold phi - 3/2. The upstream lemma phi_gt_onePointFive supplies the strict inequality phi > 1.5 that discharges the last two fields.

proof idea

The definition is a direct structure constructor. It assigns the codata_in_band field to the sibling theorem of the same name, the phi_is_golden field to the golden-ratio definition, and the two inequalities via linarith applied to the imported lemma phi_gt_onePointFive.

why it matters

This certificate completes the explicit alpha derivation inside the module and is the sole inhabitant supplied to the downstream theorem alphaProvenance_inhabited that proves the structure is nonempty. It therefore closes the provenance chain from J-uniqueness through phi and D = 3 to the numerical match with CODATA, confirming that the fine-structure constant emerges inside the predicted band without additional axioms. The construction directly supports the structural claim that alpha inverse lies in (137.030, 137.039) as required by the Recognition Science forcing steps T5-T8.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 57)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.