musicRealization
musicRealization supplies the concrete LogicRealization whose carrier is the natural numbers viewed as discrete interval steps. Researchers tracing the universal forcing chain cite it when they need an explicit arithmetic orbit realized through pitch-ratio stacking. The definition is a direct record that populates every LogicRealization field by delegating to musicCost, musicInterpret, and the inductive constructors of LogicNat.
claimThe musical realization is the structure whose carrier is the set of natural numbers, cost function is the interval-step comparison musicCost, zero element is 0, successor is the standard successor, orbit type is the inductive LogicNat with its zero and successor, and interpretation map is musicInterpret, satisfying the required axioms by reflexivity and the injectivity of successor on LogicNat.
background
LogicRealization is the interface that turns an abstract orbit into a concrete arithmetic carrier equipped with cost, step, and interpretation maps. In this module the carrier is specialized to MusicalIntervalStep, which is simply the type of natural numbers. The orbit is supplied by LogicNat, the inductive type whose constructors identity and step mirror the multiplicative orbit generated by a fixed ratio, with toNat reading off the iteration count. The module doc states that the semantic reading is pitch-ratio stacking and that the forced arithmetic is the iteration count of interval composition.
proof idea
The definition is a direct record instantiation. It assigns Carrier to MusicalIntervalStep, Cost to Nat, compare to musicCost, orbit to LogicNat, interpret to musicInterpret, and the remaining fields to the corresponding music* lemmas or LogicNat constructors. The interpret_step and orbitEquiv_step fields are discharged by rfl; orbit_no_confusion uses zero_ne_succ; orbit_step_injective uses succ_injective; orbit_induction uses LogicNat.induction; and nontrivial is proved by exhibiting the element 1 and simplifying musicCost.
why it matters in Recognition Science
This definition supplies the concrete instance that music_arith_equiv_nat uses to obtain the equivalence between the arithmetic carrier and LogicNat. It therefore closes the musical realization leg of the universal forcing construction, allowing the Peano structure forced by LogicNat to be read as interval-step arithmetic. The construction sits downstream of the ArithmeticFromLogic development and upstream of any theorem that needs an explicit orbit for interval composition.
scope and limits
- Does not derive the value of any physical constant or the phi-ladder mass formula.
- Does not treat continuous pitch spaces or non-integer interval ratios.
- Does not prove the Recognition Composition Law or any T5-T8 forcing steps.
- Does not address nontriviality beyond exhibiting a single positive-cost element.
formal statement (Lean)
37def musicRealization : LogicRealization where
38 Carrier := MusicalIntervalStep
proof body
Definition body.
39 Cost := Nat
40 zeroCost := inferInstance
41 compare := musicCost
42 zero := 0
43 step := Nat.succ
44 Orbit := LogicNat
45 orbitZero := LogicNat.zero
46 orbitStep := LogicNat.succ
47 interpret := musicInterpret
48 interpret_zero := by rfl
49 interpret_step := by
50 intro n
51 show LogicNat.toNat (LogicNat.succ n) = Nat.succ (LogicNat.toNat n)
52 rfl
53 orbit_no_confusion := by intro n h; exact LogicNat.zero_ne_succ n h
54 orbit_step_injective := LogicNat.succ_injective
55 orbit_induction := by
56 intro P h0 hs n
57 exact LogicNat.induction (motive := P) h0 hs n
58 orbitEquivLogicNat := Equiv.refl LogicNat
59 orbitEquiv_zero := rfl
60 orbitEquiv_step := by intro n; rfl
61 identity := musicCost_self
62 nonContradiction := musicCost_symm
63 excludedMiddle := True
64 composition := True
65 actionInvariant := True
66 nontrivial := by
67 refine ⟨1, ?_⟩
68 simp [musicCost]
69