Forge Intelligence

MathGenesis objects and formulas (P0)

Inventory of bundled knowledge under knowledge/math/. The registry (registry.yaml) lists three reference objects; the examples directory holds 12 JSON files including pipeline batches and pedagogy fixtures.

Updated

Registry (reference partition)

Registry object_id File object_type Partition
math.number.greatest_common_divisor gcd_definition.json definition reference
math.geometry.pythagorean_theorem pythagorean_theorem.json theorem reference
math.number.euclidean_algorithm euclidean_algorithm.json algorithm reference

Note: pythagorean_theorem.json uses canonical object_id geometry.euclidean.pythagorean_relation (registry alias points at the same file).

M06 fixture objects

object_id File Role
geometry.euclidean.equilateral_construction geometry_construction_valid.json Valid synthetic construction with ordered steps
geometry.euclidean.trisect_angle_impossible geometry_construction_impossible.json Impossible construction (no steps; construction_impossible metadata)

Physics objects migrated to PhysicsGenesis — see INTELLIGENCE-BRIDGES.md and PhysicsGenesis objects.


Reference formulas and statements

Greatest common divisor (definition)

Statement: For integers a and b, not both zero, gcd(a,b) is the unique positive integer d such that d divides a and b, and every common divisor of a and b divides d.

Formal definition: d = gcd(a,b) iff d > 0, d | a, d | b, and for every integer c, (c | a and c | b) implies c | d.

Symbol Role Domain
a input integer Integer
b input integer Integer
d greatest common divisor PositiveInteger

Assumptions: a and b are integers; not both zero.

Verification (unresolved): formal proof receipt; equivalence check with selected formal-library definition before promotion.


Euclidean algorithm (algorithm)

Statement: Given integers a and b, not both zero, repeatedly apply (x,y) ← (y, x mod y) until y=0; return |x|.

Procedure (summary):

  1. Set x = |a|, y = |b|.
  2. While y ≠ 0, replace (x,y) with (y, x mod y).
  3. Return x.

Verification (unresolved): formal correctness receipt; termination and partial-correctness obligations.


Pythagorean relation (theorem)

Statement: For a Euclidean triangle with a right angle between sides of lengths a and b and opposite side of length c, a² + b² = c².

Formal statement: right_triangle(a,b,c) -> a^2 + b^2 = c^2

Symbol Role Domain Dimension
a leg length PositiveReal L
b leg length PositiveReal L
c opposite-side length PositiveReal L

Assumptions: Euclidean plane; nondegenerate triangle; right angle between a and b.

Worked example: a=3, b=4, c=59+16=25 (positive case). Counterexample: 2,3,4 (non-right).

Geometry metadata: representation_mode: synthetic, diagram_status: illustrative, primitives include point, line, segment, triangle.

Verification (unresolved): formal geometry proof receipt.


Projectile with quadratic drag (migrated)

Canonical object: phys.simulation.projectile-quadratic-drag.v1 in knowledge/physics/. See PhysicsGenesis objects and INTELLIGENCE-BRIDGES.md.

Statement: dr/dt = v and m dv/dt = m g - (1/2) ρ C_d A ||v|| v (illustrative; hypothesis without bundled numerical receipt).


Pedagogy and pipeline examples (not standalone theorems)

File Role Key content
common_measure_curriculum.json Curriculum problem Rods of length 12 and 18 marks — find longest whole-mark common unit
common_measure_candidate.json Discovery candidate Learner formulation of common-measure relation
genesis0_batch.json library-batch Genesis-0 curriculum + discovery pair
reference_batch.json library-batch GCD, Euclidean algorithm, Pythagorean in one batch
ingestion_plan_example.json ingestion-plan Bounded reference-ingestion plan
promotion_decision_example.json promotion-decision Hard gates and promotion rationale template
variables_ingestion_plan.json Plan variant Variable substitution in ingestion templates
rendered_ingestion_messages.json Prompt fixtures Rendered system/user messages for Library Governor

Partition visibility (P0)

Per math_partition_policy.yaml:

  • Reference objects (gcd, Pythagorean, Euclidean) are not visible to learner credentials in the store API.
  • Curriculum and discovery examples use curriculum or discovery_staging partitions where learner visibility is enabled.