quantization
Every element of the subgroup generated by a nonzero integer δ admits a unique integer coefficient n such that its value equals n times δ. Modelers of quantized charges or lattice packings cite the result to guarantee unique representations in delta-subgroups. The proof extracts the coefficient via toZ, verifies the representation equation with toZ_spec, and invokes rep_unique to settle uniqueness.
claimFor any nonzero integer $δ$ and any $x$ belonging to the subgroup of integers generated by $δ$, there exists a unique integer $n$ such that the value of $x$ equals $n · δ$.
background
DeltaSub δ is the set of all integers x for which there exists an integer n satisfying x = n · δ. The module specializes this construction to δ = 1 to obtain a clean order isomorphism with the integers. The auxiliary function toZ extracts the coefficient n for any given element of DeltaSub δ, while toZ_spec records the defining equation x.val = toZ δ x · δ. The supporting lemma rep_unique states that if n · δ = m · δ and δ ≠ 0 then n = m.
proof idea
The tactic proof opens with classical reasoning and refines the goal to a triple consisting of the witness toZ δ x, the equality supplied by toZ_spec, and a uniqueness clause. The uniqueness clause assumes another integer m with x.val = m · δ, equates the two representations of x.val, and applies rep_unique to conclude that m equals toZ δ x.
why it matters in Recognition Science
The theorem supplies the unique integer coefficient required for quantization inside the ledger framework and is invoked by nobleGasZFull, decodeCoeff, J_at_phi_approx, phi_ladder_stable, conservation_is_unconditional, and loops_eq_face_pairs_D3. It therefore anchors the representation of charges and positions that feed the eight-tick octave and the derivation of D = 3. No open scaffolding questions are attached to this declaration.
scope and limits
- Does not apply when δ equals zero.
- Does not treat subgroups generated by non-integers.
- Does not supply explicit bounds on the coefficient n.
- Does not extend the uniqueness claim beyond the integer case.
formal statement (Lean)
107theorem quantization {δ : ℤ} (hδ : δ ≠ 0) (x : DeltaSub δ) :
108 ∃! (n : ℤ), x.val = n * δ :=
proof body
Tactic-mode proof.
109by
110 classical
111 -- Existence from `toZ_spec`
112 refine ⟨toZ δ x, ?eq, ?uniq⟩
113 · simpa [toZ_spec δ x]
114 · intro m hm
115 -- Uniqueness from `rep_unique`
116 have h1 : x.val = toZ δ x * δ := toZ_spec δ x
117 have h2 : x.val = m * δ := hm
118 have : m * δ = toZ δ x * δ := by rw [← h2, h1]
119 exact rep_unique (δ:=δ) hδ this
120
121end LedgerUnits
122end IndisputableMonolith