7.4. Dimensional homogeneity along the hypergraph
Three results grow in scope here, and the third capstone is the jump from the first two to the third. The curated homomorphism is proved: for a curated interaction algebra, whenever the algebra sanctions a product, the result's dimension is the product of the operands' dimensions. It holds because the algebra carries that side condition in its definition, so it is per algebra, and only for the product and quotient edges an author chose to mirror into one. The coverage command is mechanical: it walks every authored edge under a namespace across all nine witness families and evaluates each family's dimensional rule. It is total, but per edge, and its output is a report rather than a theorem. The capstone below composes both: given a well-formed hypergraph whose occurrences all carry coherent families, dimension is a homomorphism along every occurrence and hence along every path, so the dimension of every derived node and every output is the one computed from the sources' dimensions by composing the rules. A per-edge verdict says each step balances; the capstone says the whole model balances end to end — dimensional analysis of the entire algorithm as a theorem — and it covers the families the model actually uses, transcendental, power, copy and difference among them, which no interaction algebra curates. In the paradigm's words: the seal of a module says nothing undeclared enters, and homogeneity says every law traversed coheres, so an output's kind rests on declared sources through coherent laws.
Dimensional homogeneity along the hypergraph.
Let g be a well-formed provenance hypergraph and dimOf the
declared dimension of each kind, such that the declared assignment of dimensions to nodes
is homomorphic along every occurrence — the family's rule, applied to the operands'
dimensions, gives the result's: a product adds the operand exponents, a quotient subtracts
them, a reciprocal negates them, a power scales them by its exponent, a transcendental
demands dimension one, a copy and a reference preserve, a same-kind sum demands equal
operands — the verdict the coverage command reports as [coherent], stated per occurrence
and decided by the executable coherent. Then every assignment that follows the rules along
every occurrence from the same source dimensions agrees with the declared one on every
known node — every derived node, produced port and exit: the dimension of every output is
the one the rules compute from the sources' alone, and the dimension functor is a
homomorphism along every path of g. Stated over any rule algebra in the core
(Provenance.homogeneity) and instantiated on PhysLib's dimensions with the coverage
command's rules (dimRule); the hypergraph-level, total form of
the curated homomorphism, which is per edge and per algebra.
Lean code for Theorem7.4.1●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/DimensionalHomogeneity.leancomplete
theorem PropertyKindCalculus.DimensionalHomogeneity.dimensional_homogeneity {B : Type} [DimensionBasis B] [Fintype B] {ν κ : Type} [BEq ν] [LawfulBEq ν] [BEq κ] {g : PropertyKindCalculus.Provenance ν κ} (hwf : g.WellFormed) (dimOf : κ → Option (Dimension B)) (hcov : ∀ o ∈ g.occurrences, PropertyKindCalculus.Provenance.Homomorphic PropertyKindCalculus.DimensionalHomogeneity.dimRule (PropertyKindCalculus.Provenance.declaredDim dimOf g) o) {δ : ν → Option (Dimension B)} (hδ : ∀ o ∈ g.occurrences, PropertyKindCalculus.Provenance.Homomorphic PropertyKindCalculus.DimensionalHomogeneity.dimRule δ o) (hsrc : ∀ s ∈ g.sources, δ s = PropertyKindCalculus.Provenance.declaredDim dimOf g s) : (∀ x ∈ g.known, δ x = PropertyKindCalculus.Provenance.declaredDim dimOf g x) ∧ (∀ y ∈ g.outputs, δ y = PropertyKindCalculus.Provenance.declaredDim dimOf g y) ∧ ∀ i ∈ g.intros, i.tier = PropertyKindCalculus.Provenance.IntroTier.derived → δ i.node = PropertyKindCalculus.Provenance.declaredDim dimOf g i.node
theorem PropertyKindCalculus.DimensionalHomogeneity.dimensional_homogeneity {B : Type} [DimensionBasis B] [Fintype B] {ν κ : Type} [BEq ν] [LawfulBEq ν] [BEq κ] {g : PropertyKindCalculus.Provenance ν κ} (hwf : g.WellFormed) (dimOf : κ → Option (Dimension B)) (hcov : ∀ o ∈ g.occurrences, PropertyKindCalculus.Provenance.Homomorphic PropertyKindCalculus.DimensionalHomogeneity.dimRule (PropertyKindCalculus.Provenance.declaredDim dimOf g) o) {δ : ν → Option (Dimension B)} (hδ : ∀ o ∈ g.occurrences, PropertyKindCalculus.Provenance.Homomorphic PropertyKindCalculus.DimensionalHomogeneity.dimRule δ o) (hsrc : ∀ s ∈ g.sources, δ s = PropertyKindCalculus.Provenance.declaredDim dimOf g s) : (∀ x ∈ g.known, δ x = PropertyKindCalculus.Provenance.declaredDim dimOf g x) ∧ (∀ y ∈ g.outputs, δ y = PropertyKindCalculus.Provenance.declaredDim dimOf g y) ∧ ∀ i ∈ g.intros, i.tier = PropertyKindCalculus.Provenance.IntroTier.derived → δ i.node = PropertyKindCalculus.Provenance.declaredDim dimOf g i.node
**Dimensional homogeneity along the hypergraph** (the third capstone). Let `g` be a well-formed provenance hypergraph and `dimOf` the declared dimension of each kind. If the declared assignment is homomorphic along every occurrence under the coverage rules — the `[coherent]` verdict per occurrence — then every assignment that follows the rules from the same source dimensions agrees with the declared one on every known node, hence on every output and every derived node: the dimension functor is a homomorphism along every path of `g`, and every output's dimension is computed from the sources' alone.
Induction over the conjunctive closure from the sources (reachableFrom_sound, the same
principle the seal of a module rests on), one case per occurrence, closed by the rule: two
homomorphic assignments agreeing on the operands agree on the result. Well-formedness
supplies that every derived node and every output is in the closure. The coverage rows as
hypergraph data are the declared assignment declaredDim dimOf g and the per-occurrence
verdict coherent, which coherent_iff identifies with the hypothesis. Non-vacuity: the
refuted L · L → L edge as a mutant occurrence that fails the verdict and, together with
it, the conclusion — the rule-following assignment gives the output L², not the declared
L (homogeneity_witnesses). What remains an instrument is reading dimOf off the
environment's DimensionedKind registry for a harvested hypergraph, which the coverage
command does by elaboration and the theorem takes as a hypothesis.