production module

`AutoSamplingTheory.ExampleCases.SampleWiki`

6 named declarations scanned from AutoSamplingTheory/ExampleCases/SampleWiki.lean.

Imports

AutoSamplingTheory.ExampleCases.SampleWiki.Cases.IdealProximalChain

Imported by

AutoSamplingTheory.ExampleCasesTests.SampleWikiExampleCases

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

structure AutoSamplingTheory.ExampleCases.SampleWiki.SourceIdentity Compiled Not mapped

- Stable source identity attached to a SampleWiki case before mathematical formalization begins. The hashes are supplied by the source watcher rather than trusted as mathematical evidence by themselves.

structure SourceIdentity where
  stableId : String
  sourceUrl : String
  pageSha256 : String
  statementSha256 : String := ""
  deriving Repr, DecidableEq

/-- Verification stages are intentionally finer than a Boolean `verified`
flag. In particular, successful Lean elaboration precedes semantic source
review and graph assimilation. -/

AutoSamplingTheory/ExampleCases/SampleWiki.lean:30published source at 77184245109a

inductive AutoSamplingTheory.ExampleCases.SampleWiki.VerificationStage Compiled Not mapped

- Verification stages are intentionally finer than a Boolean `verified` flag. In particular, successful Lean elaboration precedes semantic source review and graph assimilation.

inductive VerificationStage where
  | discovered
  | sourcePinned
  | normalized
  | leanTarget
  | compiled
  | sourceReviewed
  | assimilated
  deriving Repr, DecidableEq

/-- Only a source-reviewed or already assimilated case is eligible to feed the
scientific theorem graph. A merely compiled theorem-shaped declaration is not
enough. -/

AutoSamplingTheory/ExampleCases/SampleWiki.lean:40published source at 77184245109a

def AutoSamplingTheory.ExampleCases.SampleWiki.admissibleForScientificGraph Compiled Not mapped

- Only a source-reviewed or already assimilated case is eligible to feed the scientific theorem graph. A merely compiled theorem-shaped declaration is not enough.

def admissibleForScientificGraph : VerificationStage → Prop
  | .sourceReviewed => True
  | .assimilated => True
  | _ => False

/-- An assimilated SampleWiki case satisfies the graph-admission contract. -/

AutoSamplingTheory/ExampleCases/SampleWiki.lean:53published source at 77184245109a

theorem AutoSamplingTheory.ExampleCases.SampleWiki.assimilated_admissible Compiled Not mapped

- An assimilated SampleWiki case satisfies the graph-admission contract.

theorem assimilated_admissible :
    admissibleForScientificGraph .assimilated := by
  trivial

/-- Compilation alone does not discharge the source-review boundary. -/

AutoSamplingTheory/ExampleCases/SampleWiki.lean:59published source at 77184245109a

theorem AutoSamplingTheory.ExampleCases.SampleWiki.compiled_not_admissible Compiled Not mapped

- Compilation alone does not discharge the source-review boundary.

theorem compiled_not_admissible :
    ¬ admissibleForScientificGraph .compiled := by
  intro h
  exact h

/-- Discovery alone is never treated as a formal mathematical certificate. -/

AutoSamplingTheory/ExampleCases/SampleWiki.lean:64published source at 77184245109a

theorem AutoSamplingTheory.ExampleCases.SampleWiki.discovered_not_admissible Compiled Not mapped

- Discovery alone is never treated as a formal mathematical certificate.

theorem discovered_not_admissible :
    ¬ admissibleForScientificGraph .discovered := by
  intro h
  exact h

end SampleWiki
end ExampleCases
end AutoSamplingTheory

AutoSamplingTheory/ExampleCases/SampleWiki.lean:70published source at 77184245109a