mapDelta_diff
The lemma establishes that the difference between two images under mapDelta equals the affine slope times the integer difference of the underlying projections toZ. Researchers deriving separations in charge or time quanta within Recognition Science unit mappings would cite it to preserve affine structure across delta subgroups. The proof expands the mapDelta definition and reduces via ring algebra plus an integer cast identity.
claimLet $δ ∈ ℤ$ with $δ ≠ 0$, let $f$ be an affine map $ℤ → ℝ$ with slope $s$ and offset $b$, and let $p, q$ lie in the subgroup of $ℤ$ generated by $δ$. Then mapDelta$(δ, f, p)$ − mapDelta$(δ, f, q)$ = $s · ((toZ(δ, p) − toZ(δ, q) : ℤ) : ℝ)$.
background
DeltaSub δ is the subgroup of ℤ consisting of all integer multiples of δ. AffineMapZ is the structure carrying a real slope and offset that defines the map n ↦ slope · n + offset. The function mapDelta composes an AffineMapZ with the projection toZ that recovers the integer coefficient of an element in the δ-subgroup, yielding a real-valued image for each subgroup element. The local setting in UnitMapping treats these subgroups as abstract placeholders for charge and time quanta. The lemma depends on the mapDelta definition and toZ projection supplied by the Scales and LedgerUnits modules.
proof idea
The tactic proof opens a calc block. It substitutes the definition of mapDelta to obtain the difference of two affine expressions, cancels the common offset by ring, factors the slope via mul_sub, and resolves the final integer-to-real cast by invoking Int.cast_sub inside a simpa.
why it matters in Recognition Science
The result is invoked by the companion lemma mapDelta_diff_toZ via simpa. It ensures that differences of mapped values remain consistent with the affine structure when constructing charge, time, and action maps from integer rungs. In the Recognition framework this supports translation between the phi-ladder and real physical quantities while preserving the eight-tick octave and D = 3 spatial structure.
scope and limits
- Does not assume any particular numerical value for slope or offset.
- Does not apply when δ equals zero.
- Does not extend the identity to maps that are not affine.
- Does not address non-integer generators or continuous subgroups.
formal statement (Lean)
34lemma mapDelta_diff (δ : ℤ) (hδ : δ ≠ 0) (f : AffineMapZ)
35 (p q : DeltaSub δ) :
36 mapDelta δ hδ f p - mapDelta δ hδ f q
37 = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by
proof body
Tactic-mode proof.
38 classical
39 calc
40 mapDelta δ hδ f p - mapDelta δ hδ f q
41 = (f.slope * (LedgerUnits.toZ δ p : ℝ) + f.offset)
42 - (f.slope * (LedgerUnits.toZ δ q : ℝ) + f.offset) := by
43 simp [mapDelta]
44 _ = f.slope * (LedgerUnits.toZ δ p : ℝ)
45 - f.slope * (LedgerUnits.toZ δ q : ℝ) := by
46 ring
47 _ = f.slope * ((LedgerUnits.toZ δ p : ℝ)
48 - (LedgerUnits.toZ δ q : ℝ)) := by
49 simpa [mul_sub]
50 _ = f.slope * ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ) := by
51 have hcast : ((LedgerUnits.toZ δ p - LedgerUnits.toZ δ q : ℤ) : ℝ)
52 = (LedgerUnits.toZ δ p : ℝ) - (LedgerUnits.toZ δ q : ℝ) := by
53 simpa using (Int.cast_sub (LedgerUnits.toZ δ p) (LedgerUnits.toZ δ q))
54 simpa [hcast]
55
56/-- Context constructors: charge (quantum `qe`) and time (τ0). -/