Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Generated Product Events

Abstract

Generated Product Events.

Definition 1.1 (Attributes come from the two actual parents).

Lean statement: D5/S3/ConceptDynamics/Spacetime/ProductNodes.generatedAttributes

Formalization. D5/S3/ConceptDynamics/Spacetime/ProductNodes.generatedAttributes (✓ std3).

Source. Repository-derived.

Commentary.

Generated time is the maximum of the two parent times plus one. Position is their sum, the Boolean sign represents the product of signed contributions, and the source is the ordered FreeMagma pair. Old attributes are copied verbatim.

Theorem 1.2 (The three literal tags separate all occurrences).

Lean statement: D5/S3/ConceptDynamics/Spacetime/ProductNodes.eventCode_injective

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Spacetime/ProductNodes.eventCode_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

The presentation includes both complete old archives and every pair of current parents. Tag two carries the literal HF pair of the two event names. The proved injection and finite presentation equivalence make this the prescribed HF archive.

Theorem 1.3 (Source coding commutes with ordered tree pairing).

Lean statement: D5/S3/ConceptDynamics/Spacetime/ProductNodes.source_code_generated

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Spacetime/ProductNodes.source_code_generated (✓ std3). ∎

Source. Repository-derived.

Commentary.

The existing source encoder represents the generated tree by its branch tag and ordered pair of source codes. Event tags do not rename natural leaves. The HF event code also commutes with the fixed set-theoretic pairing.

References