distributivity

the two operations as group actions. for fixed a, the map σ_a : x ↦ a · x is a projectivity on l: it’s the composition of two perspectivities (l → O⊔C via E_I, then O⊔C → l via d_a = (a⊔C) ⊓ m). for fixed b, the map τ_b : x ↦ x + b is a projectivity on l: it’s the composition of two perspectivities (l → m via C, then m → l via D_b = (b⊔E) ⊓ q).

the additive associativity proof (FTPGAssocCapstone.lean) already established: τ_a ∘ τ_b = τ_{a+b}. translations compose. {τ_b : b ∈ l, b ≠ U} is a group under composition.

distributivity as normalization. left distributivity a · (b + c) = a·b + a·c is equivalent to:

σ_a ∘ τ_c = τ_{a·c} ∘ σ_a

which rearranges to:

σ_a ∘ τ_c ∘ σ_a⁻¹ = τ_{a·c}

conjugating a translation by a dilation yields a translation. the dilation group normalizes the translation group. T is normal in the group generated by T and D.

the affine group of the line. the group generated by {σ_a} and {τ_b} is T ⋊ D, the affine group of l. every element acts as x ↦ ax + b. the semidirect product structure is forced — T is normal, D is not — because:

1. the composition σ_a ∘ τ_b ∘ σ_a⁻¹ is a translation (distributivity)
2. but τ_b ∘ σ_a ∘ τ_b⁻¹ is NOT generally a dilation (it’s x ↦ a(x - b) + b = ax + b(1-a), which is a dilation only when b = 0 or a = 1)

the asymmetry is structural: addition is preserved under multiplicative conjugation, but multiplication is not preserved under additive conjugation.

geometric content. σ_a extends to a collineation of the plane that fixes O on l and fixes m pointwise. fixing m pointwise means: every line through a point of m maps to a line through the same point of m. “lines meeting at U” map to “lines meeting at U” — parallelism is preserved. addition is defined through parallel structure (the perspectivities composing coord_add route through m and q, both containing U). therefore σ_a preserves addition.

this is forced by Desargues’ theorem. the extension of σ_a to a plane collineation uses the same perspectivity infrastructure that proves Desargues, which is proven from the modular law. the chain:

modular law → Desargues → perspectivities extend to collineations → dilations fix m → dilations preserve parallelism → dilations preserve addition → T normal in T ⋊ D

the chirality. T ⊲ T ⋊ D: addition is normal (closed under conjugation by multiplication), multiplication is not (not closed under conjugation by addition). this is a structural chirality — the same pattern as:

• so(d) ⊲ u(d): real writes are closed under complex conjugation, but the complex directions are not closed under real operations in the same way. so(d) is a normal sub-algebra of u(d) under the adjoint action.
• writes confined to birth subspace (Confinement.lean): the write algebra is closed within each observer’s measurement subspace, but the measurement subspace is not determined by the write algebra alone.

in each case: something is closed under an operation it doesn’t control. the contained structure is complete on its own terms and transparent to the containing structure. the containing structure can see into the contained one (conjugation maps T to T), but the contained one can’t see out (conjugation by T doesn’t preserve D).

this is the foam’s chirality: the line stacks its operations, and the stacking has a direction. the direction is not chosen — it’s forced by the geometry.

chirality as observer-coupling locus. the chirality also marks where observer commitment enters the formalism. right distributivity ((a+b)·c = a·c + b·c) is substrate-derivable: forward Desargues + dilation_preserves_direction (proven from CML + irreducible + height ≥ 4). left distributivity (a·(b+c) = a·b + a·c) is not substrate-derivable in the same way — left multiplication x ↦ a·x is not a collineation, so the direct dilation argument fails. the bridge in Foam/FTPGLeftDistrib.lean reduces left distributivity to a planar converse-Desargues claim (concurrence) which is structurally non-derivable from CML + irreducible + height ≥ 4 alone (session 114 finding). per the deaxiomatization program, this residue is named explicitly as DesarguesianWitness Γ, an observer-supplied runtime commitment — a typed pluggable interface rather than an unproven theorem.

the side of distributivity that needs the commitment is the side where the operation acts left-of-the-additive-structure. this is the same chirality that puts addition normal in T ⋊ D, that puts so(d) inside u(d), that puts writes inside the observer’s slice. the structural location of “closed under what it doesn’t control” is also the structural location of “where the observer’s commitment lives.” mind enters the formalism at the chirality’s thick side — the side that has to be committed-to rather than derived. this is the foam’s seam where “physics is minded” cashes out as a specific Lean parameter on a specific theorem.

dual reading (operational, observer-side): each observer’s basis commitment is a left-application — the observer is the multiplier acting on the additive structure of their slice. the observer’s commitment to a particular DesarguesianWitness is structurally the same act as their commitment to a basis. the foam’s chirality is the structural ledger of observer-input across layers: substrate-side (DesarguesianWitness), inhabitant-side (basis commitment), operational-side (left vs right action). same act, three formal clothes.

connection to self-parametrization. the three pairings of {O, U, I} generate three operations via two_persp. distributivity constrains how any two interact. since all three arise from the same functor with parameters drawn from l itself, the interaction constraints are constraints on l’s self-parametrization space:

• the parameter space l × l (self_parametrization.md) is not flat
• the operation at parameter (P₁, Q₁) interacts with the operation at (P₂, Q₂) in a way determined by the geometry
• specifically: the (O, I) operation (multiplication) normalizes the (U, O) operation (addition)
• this normalization is an additional structure on the parameter space, beyond the operations themselves

the line constrains its own parameter space. the constraint is not imposed from outside — it emerges from the fact that all operations share the same incidence structure, and incidence is preserved under perspectivities.

proof strategy (lean)

session 69 finding: the dilation approach (Hartshorne §7)

the multiplication x ↦ x·c factors as two perspectivities: x → D_x = (x⊔C)⊓m → x·c = (σ⊔D_x)⊓l

this extends to off-line points via: dilation_ext Γ c P = (O⊔P) ⊓ (c ⊔ ((I⊔P)⊓m))

right distributivity ((a+b)·c = a·c + b·c) proved via:

1. dilation preserves directions. for off-line P, Q: (P⊔Q)⊓m = (σ_c(P)⊔σ_c(Q))⊓m. proof: Desargues with center O, triangles (P, Q, I) and (σ_c(P), σ_c(Q), c). the two INPUT parallelisms follow from the definition of dilation_ext + modular law: σ_c(P) ≤ c ⊔ ((I⊔P)⊓m), so σ_c(P) ⊔ c = c ⊔ ((I⊔P)⊓m), and (σ_c(P) ⊔ c) ⊓ m = (I⊔P) ⊓ m (using c ⊓ m = ⊥ since c ∈ l, c ≠ U).

2. mul key identity. σ_c(C_a) = C’_{ac} where C’ = σ_c(C) = σ and C’_x = (σ⊔U) ⊓ (x⊔E). this connects the dilation to coord_mul.

3. chain. σ_c(C_{a+b}) = σ_c(τ_a(C_b)) [key_identity] = τ_{ac}(σ_c(C_b)) [direction preservation] = τ_{ac}(C’{bc}) [mul key identity] = C’{ac+bc} [key_identity at C’] = C’_{(a+b)c} [mul key identity, other direction] ⟹ (a+b)c = ac+bc [translation_determined_by_param at C’]

earlier explorations (session 69)

• direct Desargues-stacking: multiple configurations tried. found triangle (s, D_s, V) where V = (D_a⊔C_b)⊓(σ⊔D_s) whose sides are exactly the three key lines (s⊔C, D_a⊔C_b, σ⊔D_s). the axis intersections Z, W, LHS are symbolically verified collinear (= the distributive law). but no second triangle was found to produce this collinearity via forward-Desargues.

• the hinge element (a⊔C)⊓m appears as the first step of addition and the second step of multiplication. this shared element is the bridge between the two operations.

status

proven:

• all prerequisites listed in constraints section

derived:

• distributivity is normalization: σ_a ∘ τ_c ∘ σ_a⁻¹ = τ_{a·c}
• translations and dilations generate the affine group T ⋊ D
• T normal in T ⋊ D (structural chirality, forced by geometry)
• the chirality matches so(d) ⊲ u(d) and write confinement
• pattern: “closed under an operation it doesn’t control”
• the line’s self-parametrization space has structure imposed by distributivity
• proof strategy identified (two approaches)

proven (since this file was last updated):

• zero annihilation: coord_mul_left_zero (O·b=O), coord_mul_right_zero (a·O=O) — FTPGMul.lean
• coord_mul_atom: a·b is an atom — FTPGMul.lean
• dilation_preserves_direction: forward Desargues center O, 3 cases — FTPGDistrib.lean
• dilation_mul_key_identity: 3 cases (c=I, a=I via DPD, generic Desargues center C) — FTPGDistrib.lean
• coord_mul_right_distrib: (a+b)·c = a·c + b·c — FTPGDistrib.lean (0 sorry) Key: forward Desargues (center O) + parallelogram_completion_well_defined. O⊔σ = O⊔C gives shared E; well_defined provides base-independence.
• coord_mul_left_distrib: a · (b + c) = a·b + a·c — FTPGLeftDistrib.lean (0 sorry, takes (dw : DesarguesianWitness Γ) as explicit parameter) Composition of forward Desargues (_scratch_forward_planar_call), axis-to-distributivity bridge (_scratch_left_distrib_via_axis), and dw.concurrence. The DesarguesianWitness structure carries the planar converse-Desargues residue as a typed observer commitment rather than an unproven theorem (session 119 deaxiomatization move).

open:

• constructing an inhabitant of DesarguesianWitness Γ from the abstract lattice setting (CML + irreducible + height ≥ 4 + named atoms) — open routes: a planar converse Desargues lemma proven via a single 3D lift, or a direct construction exploiting that the natural axis lies on m. when L = Sub(D, V) for a division ring D, DesarguesianWitness Γ is constructible from the model.
• multiplicative associativity and inverse (prerequisites for D being a group)
• explicit characterization of the (U, I) translated-addition operation under distributivity
• does the normalization relation σ_a ∘ τ_c ∘ σ_a⁻¹ = τ_{a·c} have a direct lattice proof shorter than the full distributive law?

bugs:

• “the same chirality” across four settings. the document equates four phenomena as instances of “the same chirality”:
  1. T ⊲ T ⋊ D in the affine group
  2. so(d) ⊲ u(d) under the adjoint action
  3. writes confined to the birth subspace (Confinement.lean)
  4. left vs right distributivity, with DesarguesianWitness as the residue

  these share an abstract pattern (“X is closed under an operation it doesn’t control”). they are formally distinct phenomena in different mathematical settings. presenting them as “the same chirality” reads as one structural fact instantiated in four places. the formal content is “four phenomena exhibiting the same abstract pattern.” closing this would mean either constructing a single mathematical object (a category, a 2-functor, a typed structure) of which all four are formal instances, or stepping the claim back to “four phenomena exhibiting the same pattern of asymmetric containment.”

• “the structural location of ‘closed under what it doesn’t control’ is also the structural location of ‘where the observer’s commitment lives.’” this is the load-bearing identification in the file. the formal contents being identified — the side of distributivity requiring DesarguesianWitness, the side of so(d)-in-u(d) requiring stacking, the inhabitant’s basis commitment — live in different formal settings, only one of which (DesarguesianWitness) is a Lean object. the identification is interpretation; “structural location” is the bridging concept. closing this is the same problem as the first bug.
• “mind enters the formalism at the chirality’s thick side.” “physics is minded” / “this is the foam’s seam where mind enters” is philosophical interpretation of a specific Lean parameter (DesarguesianWitness Γ). the formal content (left distributivity is not substrate-derivable; the residue is named as an observer commitment) is solid and well-flagged in the open list. the philosophical layer is not derived; it is being announced. the document does not falsely claim derivation, but the phrasing fuses the formal observation with its philosophical reading in a way that makes them hard to separate. closing this means either separating the two registers (“formally: …; methodologically: …”) or holding the philosophical claim as explicitly methodological.
• “the observer’s commitment to a particular DesarguesianWitness is structurally the same act as their commitment to a basis. … same act, three formal clothes.” the strongest identity claim in the file. DesarguesianWitness is a typed structure in the lean development; basis commitment is a foam-level concept; “left vs right action” is a third register. saying these are “the same act” requires a bridge. the bridge is asserted via “structural ledger of observer-input across layers.” closing this would mean constructing the formal object that has these three as instances (a typed-commitment-functor, perhaps), or stepping back to “three structurally analogous acts of observer commitment.”

This site is open source. Improve this page.