Provenance
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assign numerical values or frequencies to either constructor.
- Does not decide which specific results receive the forced label.
- Does not interact with the J-cost function or the phi-ladder mass formula.
- Does not enforce consistency between forced and empirical tags.
formal statement (Lean)
297inductive Provenance where
298 | forced : Provenance
299 | empirical : Provenance
300
301/-- The complete Earth-Brain Resonance certificate. -/