Research note: preserve provisional type-system designs for future model re-audit and repair

[isomorphisms]

Current status — 2026-09-02

STANDING_POLICY / RESEARCH. Retain this as the durable auditability rule for provisional mathematical/type-system designs. It is not an implementation task: later systems must be able to distinguish settled, open, research-only, and not-verified claims and repair them rather than inherit prose as authority.

---

Motivation

The August 29, 2026 type-system work is intentionally being written down even where implementation may be far away. A future model may be materially better at theorem search, counterexample generation, compiler synthesis, and cross-checking mathematical assumptions. The useful artifact now is therefore not merely code; it is a durable, structured design record that a later system can audit rather than blindly inherit.

This note is about the AI/CI boundary for that workflow.

Required distinction: settled kernel vs provisional research

Design notes should explicitly mark at least:

SETTLED / algebraically routine
OPEN / representation undecided
RESEARCH / mathematical or engineering question
NOT_VERIFIED / code or compiler receipt absent

A later automated pass should not treat all prose as equal-authority specification.

Examples from today's work:

Relatively settled kernels

• signed elapsed Duration has additive abelian-group structure;
• Instant + Duration -> Instant and Instant - Instant -> Duration;
• exact unit definitions/conversions should remain exact where the standards define them exactly;
• physical dimensions normalize algebraically under multiplication/division;
• ordinary interval endpoint semantics and outward rounding are well-defined requirements;
• latitude/longitude are coordinates on a spherical/ellipsoidal object, not the ontology of location.

Deliberately open

• representation of vague phrases such as last month;
• correlated uncertainty beyond naive interval arithmetic;
• relation, if any, between measurement uncertainty and infinitesimal/dual-number structures;
• exact geofence uncertainty representation (region, cover, probability, sheaf/cosheaf, combinations);
• how much theorem-guided higher-math inference belongs in elaboration;
• exact lowering/runtime representation.

Future-model audit contract

A future automated design/rewrite pass should be encouraged to:

1. reconstruct the claimed laws and type signatures;
2. search for counterexamples and edge cases;
3. distinguish mathematical error from implementation inconvenience;
4. compare against authoritative definitions/standards where relevant;
5. preserve explicit ambiguity instead of guessing a convenient meaning;
6. produce an explanation trace for every inferred or changed semantic rule;
7. retain provenance: what came from a prior design note, what was independently derived, and what was changed;
8. add executable tests before or alongside implementation where practical;
9. report actual compile/run status honestly (NOT_VERIFIED until there is a real receipt).

The desired future behavior is closer to “AlphaGo the design space”: explore alternatives, find contradictions or stronger formulations, and propose repairs. It is not “a newer model said so, therefore overwrite history.”

Useful regression/evaluation corpus

The following examples should become long-lived semantic probes because they expose common premature erasure mistakes:

# dimensions / units
1 ft + 3 in
1/4 in + 1/16 in
gallon / second
metre / second / second
foot + second   # unresolved/incompatible dimension

# time
Instant + 5 minutes
Instant - Instant
5 minutes - 8 minutes
1 calendar month != definitionally 30 days
last month      # preserve contextual/vague semantics

# intervals / tolerance
[1,3] + [4,9] = [5,12]
x:[0,1]; x-x    # correlation/dependency probe
0.250 in ± 0.001 in

# geography
all longitudes at a pole denote the same spherical point
International Date Line periodicity
mixed datum/CRS requires an explicit transformation
uncertain location crossing a fence boundary must not become a false precise Bool

# higher-math constraint inference
presheaf restriction indices
Einstein/index-domain constraints
dimensional normalization
theorem lookup only with explicit typed hypotheses

These tests are valuable even before a full language implementation because they let future systems compare proposed designs against the same semantic targets.

Cross-links

• Explore dimensional analysis in the type system Idric#28
• Infer higher-math structures from operations, laws, and theorem constraints Idric#42
• Design note: preserve mathematical semantics through type constraints instead of erasing to scalars walnut-burgundy/computer-science#60
• Type-system design notes: spherical geometry, regions, uncertainty, and geofences dilapidated-shed/geofence#1
• Design notebook: exact intervals, outward rounding, tolerance, and dependency dilapidated-shed/intervals.idr#1

Principle

Preserve enough structure today that a better compiler/model tomorrow can audit, derive, test, and repair the design. Do not preserve ambiguity by silently choosing a placeholder meaning; preserve it explicitly as an unresolved typed/design constraint.

[isomorphisms]

Add false-precision / uncertainty audit to future-model contract

A future model reviewing these designs should explicitly challenge claims where representation precision is being mistaken for knowledge precision.

Regression question: when code prints many digits for a real-world estimate, ask what those digits mean. Separate at least arithmetic exactness on stored data, floating representation error, measurement resolution, sampling uncertainty, model/estimand uncertainty, and any declared tolerance/error budget.

For interval work, future review must also reject the shortcut interval -> Gaussian. An interval gives set-valued information only; a probability distribution or CLT conclusion requires additional probabilistic assumptions and evidence. The future system should be encouraged to identify exactly which hypotheses justify any probabilistic refinement.

Calendar design should remain downstream of this ambiguity/uncertainty work and the ecosystem survey in walnut-burgundy/computer-science#61.

[isomorphisms]

Clarification for future synthesis: know algebraic structure without forcing taxonomy into source

Future automated reasoning may recognize that signed elapsed Duration satisfies additive abelian-group laws and use that fact for normalization, property generation, theorem search, counterexample checks, or code synthesis.

Do not treat recognition of that structure as evidence that Idriç source must immediately grow Java-like inheritance or mandatory declarations such as Duration : AbelianGroup.

Preferred first-stage contract is operational and testable:

Instant + Duration -> Instant
Instant - Instant  -> Duration
Duration + Duration -> Duration
-Duration           -> Duration

The richer mathematical classification can remain external/derived knowledge until it demonstrably helps elaboration or verification.

Future-model rule: distinguish the computer knows this object has structure S from the programmer must explicitly annotate/inherit from S. The former may be useful while the latter is unnecessary notation and premature architecture.

Apply the same caution to theorem-rich material already waiting in the project (representation theory, Maschke-shaped facts, tensor/categorical structure, etc.): preserve it as available knowledge, not compulsory source hierarchy.

[isomorphisms]

Future audit probe: woodpecker scaling argument

Add Lorna Gibson's woodpecker-impact example to the long-lived research/audit corpus because it cleanly separates several kinds of reasoning that a future model should not conflate:

dimensional consistency
scaling / order-of-magnitude reasoning
explicit geometric assumptions
contact-area estimates
dynamic impact-duration effects
higher-fidelity contact / constitutive / wave mechanics

Primary starting points:

• MIT OCW Built to Peck video collection: https://ocw.mit.edu/courses/3-054-cellular-solids-structure-properties-and-applications-spring-2015/pages/woodpecker-videos/
• Gibson (2006): https://doi.org/10.1111/j.1469-7998.2006.00166.x
• later 2-D biomechanical model discussing the limits of the simple scaling/contact assumptions: https://www.frontiersin.org/journals/bioengineering-and-biotechnology/articles/10.3389/fbioe.2020.00810/full

The future-model contract should preserve the simple model as a useful approximation without silently upgrading it into established detailed biomechanics. Gibson's headline ingredients are small size, short impact duration, and brain orientation/contact area. Curvature/contact geometry, stress-wave propagation, and richer contact mechanics are plausible later questions, but should not be retroactively attributed to the simple argument.

This is a good evaluation pattern for AI-assisted mathematics/engineering work: derive what the assumptions actually imply, state which quantities are dimensionful, expose the dimensionless geometric factors, and then actively search for where the approximation breaks.

Also preserve William L. Burke's Applied Differential Geometry as the intended future geometric-mechanics reference rather than designing that subsystem now:

• https://archive.org/details/applieddifferent00burk_020
• https://www.ucolick.org/~burke/class/adg.html
• https://doi.org/10.1017/CBO9781139171786

Future audit should distinguish contact mechanics from mathematical contact geometry and should not introduce screw theory / differential-geometric mechanics into Idriç merely because those subjects are known. Wait for concrete operations and forcing examples.

Cross-links:

• Design note: preserve mathematical semantics through type constraints instead of erasing to scalars walnut-burgundy/computer-science#60
• Explore dimensional analysis in the type system Idric#28

[isomorphisms]

Concrete audit target added: isomorphisms/Idric#44. The branch has tests-first commits plus a focused edric007 compiler harness for exact dimensions/units, signed duration/instant arithmetic, and 1-D interval endpoint semantics. This is a useful future-model regression object because it clearly marks what is SETTLED versus deliberately deferred. AICI should treat the actual edric007 compile/run receipt as evidence; prose/design notes and wrapper-only CI are not sufficient.

[isomorphisms]

New audit/evaluation artifact: isomorphisms/Idric#45 adds a tests-first linear-geometry-type-core and explicitly separates SETTLED structure from OPEN representation work.

Useful new long-lived probes for future model re-audit:

# dimensioned linear algebra
x : R^n; y : R^n; x-y             # allowed
x : R^n; y : R^m; x-y, n != m     # must require an explicit map / fail to elaborate

# approximation
residual(a,b)                       # mathematical value
within(a,b,epsilon)                 # epsilon remains explicit; do not guess it

# orthogonal structure
reflection * reflection -> SO(n)
O(n+1) action on S^n -> S^n

# spheres
rank H^k(S^n;Z)                     # S^0 edge case explicit
chi(S^odd)=0; chi(S^even)=2
# do not invent different additive cohomology ranks merely from parity

# quaternions
ij = k; ji = -k
unit quaternion -> SO(3)

# CP^n
real-dim CP^n = 2n
CP^n = S^(2n+1)/S^1                # named standard quotient fact
rank H^(2k)(CP^n;Z)=1 for 0<=k<=n

# named theorem boundary
embedded S^1 in S^2 -> exactly two complement components
(R^n)^+ ~= S^n

The implementation deliberately uses exact integer-coordinate samples embedded in real spaces so it does not accidentally freeze a Float16/32/64 policy. General real scalars, arbitrary Givens/Householder parameters, projections, full projective quotient machinery, and theorem provenance remain OPEN.

The PR has a real compiler harness (edric008) and is presently NOT_VERIFIED while CI is running. That status should be changed only after an actual compiler receipt.

[isomorphisms]

PASS receipt for the concrete audit target isomorphisms/Idric#44: feature head a3ffc1c03e040e31a0867d473611b1bf8960cca0 was tested in PR merge commit 59ad1d9c83028ca1dbdb8ba50f486cdd7dca9425 by workflow run 33277502908, job 99166698046. Full ./edric all bootstrap succeeded and the focused new test reported idris2/basic/edric007: success 00.854s, 1/1 tests successful. This receipt covers exact units/dimensions, signed Instant/Duration arithmetic, open/closed rational intervals, and the separate nilpotent dual-epsilon law. The only post-semantic correction was chmod on the test runner; no pinned mathematical equation was weakened.