33.4. What the kind algebra rests on — the edge audits🔗

The boundary audit asks where the calculus is left. These ask what it rests on — the laws under which two kinds may meet without a crossing.

A kind-level law — ProductKind k₁ k₂ k, a KindMul table entry, a PowerKind — is authored, not derived. The calculus signs any ratio-scale triple its author writes, exactly as a proof assistant accepts any axiom its author declares, and for the same reason: a claim about which physical quantities compose to which is not something a type checker can settle. What follows from that is not that the claims go unchecked, but that they must be enumerable.

#kind_edges k is that enumeration, per kind. It finds all three authoring styles in one scan over constant types — named witness theorems, the _proof_N auxiliaries Lean lifts out of call-site witnesses, and operator-table instances — so a reader sees every edge a kind participates in regardless of how it was written. This is what makes the Algebra column of the kind tables below worth reading: a kind whose Algebra cell is empty supports no arithmetic at all.

#kind_dimensional_coverage ns … then cross-checks those edges against the dimension layer, and it is the one place an authored edge can be refuted rather than merely listed. Each edge's kinds are resolved to their declared dimensioned kinds and the family's rule is evaluated in PhysLib's Dimension group — products add exponents, quotients subtract, powers scale by the rational exponent, a transcendental demands dimension one on both sides. An edge reports as:

[coherent]      relPermKind · relPermKind → relPermSqKind
[parametric]    pureNumber · k → k
⚠ UNDIMENSIONED angFreqKind · relaxTimeKind → dimlessKind — no DimensionedKind for: relaxTimeKind
⚠ INCOHERENT    angFreqKind · relaxTimeKind → angFreqKind
⚠ CONFLICTING   … — disagreeing DimensionedKinds for: …

[parametric] is generic vocabulary — an edge quantified over a kind variable has no fixed dimensional content, and its instantiations are audited as their own rows. The two ⚠ verdicts that matter are different failures: undimensioned is a coverage gap, an edge nobody mirrored into the dimension layer, while incoherent is a genuine error, T⁻¹ · T = T⁻¹ asserted where the group says otherwise.

The division of labour with the curated interaction algebras is worth stating, because the two look similar and are not. This command is total and mechanical: it can only affirm that an edge's dimensions balance, and every dimension-one triple balances trivially — which is most of a soil-moisture model. An InteractionAlgebra is curated: it says which products are physically sanctioned, which is the thing dimensional analysis discards and no walk can recover. Coverage is checked; curation stays authored.

#kind_dimensional_clean ns… is the coverage report's gate, and stands to it exactly as #kind_boundary_clean stands to the boundary audit: no message, nothing pinned, it throws while any edge in scope is undimensioned, conflicting or incoherent. [parametric] does not fire it. It has one false alarm, and the error message says so: both the edges and the DimensionedKind declarations are harvested from the environment, so a module that reaches an edge but not the module declaring its kinds' dimensions reports that edge undimensioned while the codebase is coherent. That is the same import-closure sensitivity the generated indexes have, pointing the other way — an under-imported report silently misses rows, an under-imported gate invents violations. The asymmetry is the safe one, because a false alarm is loud and a silent omission is not.