struct-continues

hypermath | formal-universality | dictionary

What it is

struct-continues(x, y) :: Prop asserts that x was produced by applying □ (ground) to something that y also produced by applying □ to — equivalently, that x and y share a common generator in the apply-chain. It is the semantic content proposed for the similar relation (`~~`). The actual L0 close only states struct-continues(x, ground) iff x ~~ ground. It supplies no arbitrary-pair biconditional from two ground-continuation facts. Such a biconditional would define a transitive relation, unlike general nonempty continuation overlap.

struct-continues :: Form -> Form -> Prop
-- Semantically closed in L0 Section VI.

What it is not

• Not continuation in the programming-language sense (continuations in CPS). No call stack, no return address. This is a structural generative property.
• Not inheritance in OOP. No class hierarchy, no polymorphism.
• Not the same as struct-orbits. struct-continues is about the generative chain; struct-orbits is about double-application orbit return (ax-box).

What it clarifies

Grounds the similar relation: similar is declared as an opaque in L0 Section V and closed via struct-continues in Section VI. Without struct-continues, ~~ would have no semantic content.

Concrete example

struct-continues(apply(ground), ground)  -- FORM, L0 Section III (ax-sim derivation)
-- apply(ground) struct-continues ground because apply(ground) was generated by
-- □ applied to ground. They share the generator.

Visualization

A river continues from its source spring. You can trace the water in the river back to where the spring is. The river struct-continues the spring. The spring also struct-continues itself (ax-ground-self). Anything downstream struct-continues the spring.

Speculation

Whether struct-continues can be replaced by `~~` as primitive — collapsing the opaque and the relation into one declaration — is structurally interesting but not yet derived. If ~~ is primitively sufficient, struct-continues dissolves and the Section VI closes become axioms rather than semantic assignments. This links struct-continues to struct-distinct in a minimality question: what is the irreducible set of structural predicates needed at L0?