Base: TimeLordRaps/hypermath commit
819f6856101c91fb3f0f4d25126e2f7329137b53. Scope: four root .hm layers,
their Lean translation, directly related dictionary entries, and the selected
precursor mathematical sources. This is an assisted internal review, not an
external peer review or a consistency/completeness certificate.
Commit bf22cb89cf6243e29e7788e9d09c83621dfbf6bb accidentally removed L1's
deriver/matrix block and left truncated text while removing other declarations.
The block was recovered from
e587fefc871e4c4a067303e41c159894bc55f5fd. Its text is unchanged apart from
the section numeral. deriver, D, D-is-reflexive, and D-spans-ground
now each appear once. The stray VIII and duplicated trailing 1, 2505.
fragment were removed. The deliberately removed unrelated primitives remain
removed. Restoring a purported derivation does not prove it.
The original bounded build failed: bodyless opaque declarations attempted
to obtain unspecified inhabitants. Source-declared uninterpreted primitives
are now explicit Lean parameter axioms, making their assumption status
visible. The logical clauses and unresolved theorem obligations remain
separate. No missing theorem was replaced with an axiom.
Mechanical repairs address iteration syntax, incorrectly typed proof terms,
and the path/form mismatch in the limit-path clause. The source's start
and end projections are represented explicitly rather than confusing a
path with a form or its length with its endpoint. This does not prove the
missing infinite-path laws. The audit command reports exact current counts
and axiom dependencies, including sorryAx where a proof remains unfinished.
The README now states the stronger research objective and the actual
translation status. Dictionary corrections distinguish structural distinction
from ambient inequality, restore the restricted ground-continuation bridge,
and expose the unproved translation of native propositions to Lean's Prop.
The original layer FORM labels remain source claims; they are not presented
as mechanical verification results.
| ID | Finding | Evidence and next obligation |
|---|---|---|
| M1 | Universal operand asymmetry conflicts with identity in the intended nontrivial congruence structure. | L2 ax-seq-asymm and ax-seq-identity: if a is not congruent to ground, the first forbids congruence between a+ground and ground+a; the identity laws and symmetric/transitive congruence require it. State the intended scope of noncommutativity. No axiom was silently weakened. |
| M2 | Strong self-return is assumed during its purported derivation. | L3 deriver-cycle-is-closed promotes similarity to congruence/simulation without a preservation theorem. A two-step return also does not imply that each single edge identifies its endpoints. Terminal self-derivation depends on this gap. |
| M3 | Finite and transfinite path contracts disagree. | L1 defines derivability by a finite chain; L2 declares finite paths; L3 describes an infinite path in that same type. Its limit description claims derivability while excluding finite congruent reachability. Separate and connect these contracts explicitly. |
| M4 | The written limit clauses omit their advertised content. | L3's limit-path clause omits the infinite-prefix conditions in its comments; its leastness clause does not assert the upper-bound property. An abstract object named ordinalLimit does not supply these facts. |
| M5 | Self-representation crosses sorts without a defined conversion. | L0 applies syntax : Form -> Prop to predicates/functions without reification. L2 uses proposition-valued entries of D as paths. Define representation and evidence extraction, then prove their preservation properties. |
| M6 | Similarity return does not prove a finite universe or terminating normalization. | The cited relational laws admit natural-number forms with successor and universal similarity, retaining infinitely many distinct forms. Decidable comparison, finite scope, strict decrease, and normal-form properties are separate obligations. |
| M7 | Reachability transitivity and directionality need additional arguments. | Finite reachability up to congruence need not compose unless apply respects congruence. Lack of a reverse proof is not proof of its negation. The finite probes below reproduce failures of these implications. |
| M8 | Path observation preservation is underspecified. | L2 compares endpoint, trace, and cost using similarity, while describing identical observations. Specify exactly which observations must agree for reuse and compression. |
These findings concern the stated implications and intended semantics. A countermodel of selected relational assumptions is not a model of every unwritten intended property of the framework. Conversely, an intended property does not repair a proof until stated and justified.
n*n-n=n has solutions zero and
two. Interpreting 2^(n*n-n) as independent off-diagonal binary choices does
not establish a bijection with derivation paths.n, let c(n)=2^(n*n-n). The code
`sum(c(j) for j