exp_67144_lt_824_hypothesis
plain-language theorem explainer
The declaration encodes the hypothesis that exp(6.7144) is strictly less than 824.2 as a proposition. Researchers deriving the electron mass from the Recognition Science forcing chain cite this bound to close a numerical step in the T9 necessity argument. The declaration is introduced by direct definition of the inequality with no lemmas or tactics applied.
Claim. The hypothesis that $exp(6.7144) < 824.2$ holds.
background
The module proves that the electron mass formula is forced from T8 ledger quantization and geometric constants derived in earlier theorems. This supplies one concrete numerical hypothesis inside the inequality chain for that forcing argument. Upstream, the Hypothesis structure from the classical bridge fluids module bundles constants and functionals together with projection-defect and energy-control conditions for the Galerkin state model; the supplied doc-comment states that this is exactly the data needed to build a CPM LawOfExistence model.
proof idea
The declaration is a direct definition of the Prop. No lemmas are applied and no tactics are invoked; the statement simply records the target inequality.
why it matters
This hypothesis is the target proved by the theorem exp_67144_lt_824, which splits the argument at 6 and applies the exponential addition formula. The result feeds the T9 necessity theorem establishing that the electron mass is forced by the Recognition framework from T8 onward. It closes a numerical verification step that sits between the phi-ladder mass formula and the alpha-band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.