Provenance
plain-language theorem explainer
The Provenance inductive type supplies two constructors to tag results in the Earth-Brain Resonance analysis as forced by the Recognition Science axioms or empirical. Modelers comparing Schumann harmonics to the zero-parameter formula f(n) = (4n-1)phi + 3 would cite it to keep the distinction between T6/T8 derivations and measured frequencies explicit. The declaration is a direct inductive definition that introduces the tags with no further structure or proof obligations.
Claim. The inductive type $Provenance$ is equipped with two constructors: $forced$ and $empirical$.
background
The Earth-Brain Resonance module matches the five measured Schumann harmonics (7.83, 14.3, 20.8, 27.3, 33.8 Hz) to the zero-parameter expression f(n) = (4n-1)phi + 3. Here D = 3 is the spatial dimension forced at T8, phi is the self-similar fixed point fixed at T6, and the spacing 4phi follows from the eight-tick octave. The upstream complete predicate from the SAT backpropagation module asserts that every variable in a state has been assigned, supplying a completeness notion used to certify forced components.
proof idea
This is a direct inductive definition. The two constructors forced and empirical are introduced with no lemmas, tactics, or reduction steps.
why it matters
Provenance supports the EarthBrainResonanceCert structure that packages the formula, the identity 3phi^2 = phi^4 + 1, and the spacing bounds 6.472 < 4phi < 6.476. It distinguishes results forced by the Recognition Composition Law and T8 from empirical checks, consistent with the module claim that the formula uses only RS-forced quantities. The label also appears in the alpha constant definition and the spacing_bounds theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.